Skip to content

Commit 99d3640

Browse files
committed
Improve Coq / Rocq welcome scrubbing.
Signed-off-by: Rodolphe Lepigre <[email protected]>
1 parent 7eab498 commit 99d3640

File tree

1 file changed

+2
-2
lines changed
  • test/blackbox-tests/test-cases/coq/vos-build.t

1 file changed

+2
-2
lines changed

test/blackbox-tests/test-cases/coq/vos-build.t/run.t

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88
coqc foo.vos
99
coqc bar.vos
1010

11-
$ cat foo.v | dune coq top -- foo.v 2>/dev/null | sed '/^Welcome to Coq/d'
11+
$ cat foo.v | dune coq top -- foo.v 2>/dev/null | sed '/^Welcome/d'
1212
mynat is defined
13-
$ cat bar.v | dune coq top -- bar.v 2>/dev/null | sed '/^Welcome to Coq/d'
13+
$ cat bar.v | dune coq top -- bar.v 2>/dev/null | sed '/^Welcome/d'
1414
mynum is defined
1515

1616
$ dune clean

0 commit comments

Comments
 (0)