Skip to content

Commit

Permalink
test suite printers test ignore welcome message
Browse files Browse the repository at this point in the history
The "Welcome to Coq" message can contain the current git branch which
leads to a failure if the branch contains the string "error"

Gitlab CI seems to detach HEAD so this is not observable there, but
macOS CI does show this issue
https://github.com/SkySkimmer/coq/actions/runs/12713505909/job/35442669137

(when compiling locally your `revision` is probably some old thing)
  • Loading branch information
SkySkimmer committed Jan 10, 2025
1 parent 6e32b07 commit 52414f2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion test-suite/misc/printers.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
f=$(mktemp)
{
printf 'Drop.\n#go;;\nQuit.\n' | "${BIN}rocq" repl-with-drop -q
} 2>&1 | tee "$f"
} 2>&1 | grep -a -v "Welcome to Coq" | tee "$f"

# if there's an issue in `include_utilities`, `#go;;` won't be mentioned
# if there's an issue in `include_printers`, it will be an undefined printer
Expand Down

0 comments on commit 52414f2

Please sign in to comment.