aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile
diff options
context:
space:
mode:
authorWilliam Lawvere2017-07-01 22:10:46 -0700
committerWilliam Lawvere2017-07-01 22:10:46 -0700
commit80649ebaba75838bfd28ae78822cd2c078da4b23 (patch)
treeac29ab5edd3921dbee1c2256737347fd1542dc67 /test-suite/coq-makefile
parentc2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff)
parent35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff)
Merge remote-tracking branch 'upstream/trunk' into trunk
Diffstat (limited to 'test-suite/coq-makefile')
-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 afdb32e7cf..53dc963997 100644
--- a/test-suite/coq-makefile/arg/_CoqProject
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -1,7 +1,7 @@
-R theories test
-R src test
-I src
--arg "-compat 8.4"
+-arg "-w default"
src/test_plugin.mlpack
src/test.ml4