Use provided PHPversion

DOMjudge · Dec 4, 2024 · d5e8126 · d5e8126
1 parent e60aa86
commit d5e8126
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/.github/jobs/baseinstall.sh b/.github/jobs/baseinstall.sh
@@ -4,11 +4,15 @@
 
 export version="$1"
 db=${2:-install}
+phpversion="${3}"
 
 set -eux
 
+if [ -z "$phpversion" ]; then
 PHPVERSION=$(php -r 'echo PHP_MAJOR_VERSION.".".PHP_MINOR_VERSION."\n";')
-export PHPVERSION
+fi
+
+show_phpinfo "$PHPVERSION"
 
 section_start "Run composer"
 export APP_ENV="dev"