Enhancement: Build documentation on GitHub Actions

Closes GH-9.

Author: localheinz

.github/workflows/integrate.yaml

@@ -0,0 +1,56 @@
+# https://docs.github.com/en/actions
+
+name: "Integrate"
+
+on:
+  pull_request: null
+  push:
+    branches:
+      - "master"
+
+jobs:
+  build:
+    name: "Build"
+
+    runs-on: "ubuntu-latest"
+
+    continue-on-error: true
+
+    strategy:
+      matrix:
+        language:
+          - "de"
+          - "en"
+          - "es"
+          - "fr"
+          - "it"
+          - "ja"
+          - "pl"
+          - "pt_br"
+          - "ro"
+          - "ru"
+          - "tr"
+          - "uk"
+          - "zh"
+
+    steps:
+      - name: "Checkout"
+        uses: "actions/checkout@v2"
+        with:
+          path: "doc-base"
+
+      - name: "Checkout php/doc-${{ matrix.language }}"
+        uses: "actions/checkout@v2"
+        with:
+          path: "${{ matrix.language }}"
+          repository: "php/doc-${{ matrix.language }}"
+
+      - name: "Checkout php/doc-en as fallback"
+        if: "matrix.language != 'en'"
+        uses: "actions/checkout@v2"
+        with:
+          path: "en"
+          repository: "php/doc-en"
+
+      - name: "Build documentation for ${{ matrix.language }}"
+        run: "php8.0 doc-base/configure.php --disable-libxml-check --enable-xml-details --redirect-stderr-to-stdout --with-lang=${{ matrix.language }}"

configure.php

@@ -234,7 +234,15 @@ function print_xml_errors($details = true) {
 $workdir = $srcdir;
 $basedir = $srcdir;
 $rootdir = dirname($basedir);
-if (basename($rootdir) == 'doc-base') {
+
+/**
+ * When checking out this repository on GitHub Actions, the workspace  directory is "/home/runner/work/doc-base/doc-base".
+ *
+ * To avoid applying dirname() here, we check if we are running on GitHub Actions.
+ *
+ * @see https://docs.github.com/en/free-pro-team@latest/actions/reference/environment-variables#default-environment-variables
+ */
+if (getenv('GITHUB_ACTIONS') !== 'true' && basename($rootdir) === 'doc-base') {
     $rootdir = dirname($rootdir);
 }