aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-05 14:25:10 +0100
committerPierre-Marie Pédrot2018-11-05 14:25:10 +0100
commitea678521c9eda7acde3a0276e0cec0931dbc6416 (patch)
treecbc2baf5777992a7e81e24a662dfce5db311d6a2 /test-suite
parentafc3e334c02cbbbe395387ff7110a296dce6c9f6 (diff)
parente2e7fea91f3af5dcf62052078da65489b796e9e2 (diff)
Merge PR #8870: Pass native and VM flags to the kernel through environment
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/coq-makefile/native1/_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject
index 847b2c00a9..3dfca7ffc0 100644
--- a/test-suite/coq-makefile/native1/_CoqProject
+++ b/test-suite/coq-makefile/native1/_CoqProject
@@ -2,6 +2,7 @@
-R theories test
-I src
-arg -native-compiler
+-arg yes
src/test_plugin.mlpack
src/test.mlg