aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/coqdoc2/run.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/coqdoc2/run.sh')
-rwxr-xr-xtest-suite/coq-makefile/coqdoc2/run.sh2
1 files changed, 0 insertions, 2 deletions
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index d6bb52bb4..e8291c89d 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp"
sort -u > desired <<EOT
.
./test
-./test/test_plugin.cma
./test/test_plugin.cmi
-./test/test_plugin.cmo
./test/test_plugin.cmx
./test/test_plugin.cmxs
./test/test.glob