1 files changed, 0 insertions, 36 deletions
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
deleted file mode 100755
index e48f704a2..000000000
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-cat > _CoqProject <<EOT
--I src/
-
-./src/test_plugin.mllib
-./src/test.ml4
-./src/test.mli
-EOT
-
-mkdir -p src
-
-cat > src/test_plugin.mllib <<EOT
-Test
-EOT
-
-touch src/test.mli
-
-cat > src/test.ml4 <<EOT
-DECLARE PLUGIN "test"
-
-let _ = Pre_env.empty_env
-EOT
-
-${COQBIN}coq_makefile -f _CoqProject -o Makefile
-cat Makefile.conf
-
-if make VERBOSE=1; then
-  # make command should have failed (but didn't)
-  exit 1
-else
-  # make command should have failed (and it indeed did)
-  exit 0
-fi