Fix test case for coqtop dependency recompilation.

Signed-off-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
ocaml · Apr 6, 2022 · efc912c · efc912c
1 parent 84295f1
commit efc912c
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t b/test/blackbox-tests/test-cases/coq/coqtop-recomp.t/run.t
@@ -26,10 +26,13 @@ https://github.com/ocaml/dune/pull/5457#issuecomment-1084161587).
   $ dune coq top --display short --toplevel echo dir/bar.v
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
   $ dune clean
-  $ (cd dir && echo "TESTCASE_ROOT=$TESTCASE_ROOT" && dune coq top --display verbose --toplevel echo bar.v)
+  $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
+  Entering directory '..'
         coqdep dir/bar.v.d
         coqdep dir/foo.v.d
           coqc dir/.foo.aux,dir/foo.{glob,vo}
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
-  $ (cd dir && dune coq top --display short --toplevel echo bar.v)
+  $ (cd dir && dune coq top --root .. --display short --toplevel echo dir/bar.v)
+  Entering directory '..'
   -topfile $TESTCASE_ROOT/_build/default/dir/bar.v -R $TESTCASE_ROOT/_build/default/dir basic
+