Merge branch 'topic/require_issue' into 'master'

CI: require an issue in the MR descriptions

See merge request eng/ide/gtkada!12

Author: setton

.gitlab-ci.yml

@@ -1,6 +1,18 @@
 stages:
   - build
 
+issue-check:
+  services:
+    - image:e3
+  stage: build
+  interruptible: true  # Cancel job if the branch is pushed
+  variables: # do not checkout the git repository, not needed
+    GIT_STRATEGY: none
+  rules: # Launch only on merge requests
+    - if: $CI_PIPELINE_SOURCE == 'merge_request_event'
+  script:
+    - require_issue # launch the verification
+
 build:
   services:
      - image:gtk-deps