Merge PR coq#19142: ci-wrapper: call make-one-time-file directly inst…

…ead of explicitly using python Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jun 24, 2024 · 822f40d · 822f40d
2 parents 2662a33 + 1f15a16
commit 822f40d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
@@ -48,7 +48,7 @@ fi
 code=$?
 echo 'Aggregating timing log...'
 echo
-python ./tools/make-one-time-file.py --real "$CI_NAME.log"
+tools/make-one-time-file.py --real "$CI_NAME.log"
 if [ "$CI" ] && ! [ $code = 0 ]; then
   set +x