Small CI fixes

This commit is contained in:
2023-01-18 22:04:02 +08:00
parent 54b979aa0b
commit ec8333b223
2 changed files with 3 additions and 3 deletions

View File

@@ -7,7 +7,7 @@ ecabal() {
}
nonfatal() {
"$@" || "$@ failed"
"$@" || "$* failed"
}
sync_from() {