aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/arg/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/arg/_CoqProject')
-rw-r--r--test-suite/coq-makefile/arg/_CoqProject2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject
index 53dc963997..ed31a58247 100644
--- a/test-suite/coq-makefile/arg/_CoqProject
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -4,7 +4,7 @@
-arg "-w default"
src/test_plugin.mlpack
-src/test.ml4
+src/test.mlg
src/test.mli
src/test_aux.ml
src/test_aux.mli