CI: check the XML structure of the PR head, not of the merge commit (#3193)

On a pull_request event, actions/checkout defaults to refs/pull/N/merge,
whose second parent is master. The BASE...HEAD diff therefore also lists
every file landed on master since the last push to the PR, and feeds them
to check-structure.php. A pull request touching a single non-XML file was
seen sending 294 unrelated .xml files to the check, failing on drift it
did not introduce.

Checking out the head sha restores the diff to the commits of the PR.

The expected directory layout is now noted in the workflow itself.

Author: lacatoire

.github/workflows/check-xml.yml

@@ -19,9 +19,17 @@ jobs:
     name: "Check XML"
     runs-on: ubuntu-22.04
     steps:
+      # doc-fr à la racine, doc-en dans le sous-répertoire en/ : c'est
+      # l'arborescence attendue par check-structure.php. Le ref explicite
+      # prend la tête réelle de la PR, et non le commit de fusion que
+      # actions/checkout construit par défaut : ce dernier a master pour
+      # deuxième parent, donc le diff plus bas y verrait aussi tous les
+      # fichiers arrivés sur master depuis le dernier push de la PR.
+
       - name: "Checkout php/doc-fr"
         uses: actions/checkout@v4
         with:
+          ref: ${{ github.event.pull_request.head.sha }}
           fetch-depth: 0
 
       - name: "Checkout php/doc-en"