Add base_url to enable opensearch on documentations

Signed-off-by: William Desportes <williamdes@wdes.fr>

develdocs/build.sh

@@ -28,6 +28,7 @@ for repo in phpmyadmin sql-parser motranslator shapefile simple-math ; do
     --cache-dir "$BUILDER_REPO/develdocs/tmp/$repo/" \
     --docs-branch "master" \
     --slug "phpmyadmin/$repo" \
+    --base-url "https://develdocs.phpmyadmin.net/$repo/" \
     --output-config "$BUILDER_REPO/develdocs/doctum-$repo.php"
     # Render
     nice -19 "$BUILDER_REPO/develdocs/vendor/bin/doctum.php" update --force --ignore-parse-errors "$BUILDER_REPO/develdocs/doctum-$repo.php"

develdocs/doctum.php

@@ -1,6 +1,6 @@
 #!/usr/bin/php
 <?php
-$_CLI = getopt('', ['slug:', 'root:', 'build-dir:', 'cache-dir:', 'docs-branch:', 'output-config:', 'title::', 'title-of-composer']);
+$_CLI = getopt('', ['slug:', 'root:', 'base-url:', 'build-dir:', 'cache-dir:', 'docs-branch:', 'output-config:', 'title::', 'title-of-composer']);
 
 $SOURCE = 'src';
 
@@ -30,6 +30,7 @@
     'cache_dir'            => '%s',
     'version'              => '%s',
     'remote_repository'    => new GitHubRemoteRepository('%s', '%s'),
+    'base_url'             => '%s',
 ]);
 EOT;
 
@@ -43,7 +44,8 @@
     $_CLI['cache-dir'],
     $_CLI['docs-branch'],
     $_CLI['slug'],
-    $root
+    $root,
+    $_CLI['base-url']
 );
 
 file_put_contents($_CLI['output-config'], $output);