From fb7b11089d79403c04da4bfe3b2b25e334e1f16d Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Mon, 20 Mar 2023 23:03:24 +0100 Subject: [PATCH] Remove [dune coq top] test with symbolic links. This use-case was always weird, and expanding symbolic links is not always what we want. For instance, there can be problems if we use symbolic links in a dune workspace. Signed-off-by: Rodolphe Lepigre --- .../test-cases/coq/coqtop/coqtop-ln.t | 18 ------------------ 1 file changed, 18 deletions(-) delete mode 100644 test/blackbox-tests/test-cases/coq/coqtop/coqtop-ln.t diff --git a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-ln.t b/test/blackbox-tests/test-cases/coq/coqtop/coqtop-ln.t deleted file mode 100644 index 33e94a9fd1ce..000000000000 --- a/test/blackbox-tests/test-cases/coq/coqtop/coqtop-ln.t +++ /dev/null @@ -1,18 +0,0 @@ -Running the Coq Toplevel with an absolute path containing a symbolic link. -This addresses a failure case reported by @MackieLoeffel in #5457 (see -https://github.com/ocaml/dune/pull/5457#issuecomment-1084149057). - - $ mkdir dir - $ ln -s dir sl - $ cat >dir/foo.v < Definition mynat := nat. - > EOF - $ cat >dir/dune-project < (lang dune 3.0) - > (using coq 0.3) - > EOF - $ cat >dir/dune < (coq.theory - > (name basic)) - > EOF - $ cd sl && dune coq top $PWD/foo.v > /dev/null 2> /dev/null