Skip to content

Commit 12e8278

Browse files
committed
Fixup
1 parent 92d0e02 commit 12e8278

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

.github/jobs/ci_settings.sh

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,15 @@ mysql_user () {
3434
echo "$1" | mysql -udomjudge -pdomjudge ${2:-} | tee -a "$ARTIFACTS"/mysql.txt
3535
}
3636

37+
show_phpinfo() {
38+
phpversion=$1
39+
section_start "Show the new PHP info"
40+
update-alternatives --set php /usr/bin/php"${phpversion}"
41+
php -v
42+
php -m
43+
section_end
44+
}
45+
3746
section_start () {
3847
if [ "$#" -ne 1 ]; then
3948
echo "Only 1 argument is needed for GHA, 2 was needed for GitLab."

0 commit comments

Comments
 (0)