aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-03 14:52:20 +0100
committerGaëtan Gilbert2020-02-03 14:52:20 +0100
commit1c1c04d0e3e02ce461fb953f08e2d8c68e52ee63 (patch)
tree655aa6765cdba78618a3f9bf7523237ac31846dc
parent45f0dc36a749371de35a5d4b998e1305f47e3beb (diff)
parentb35030760cadd96a968e04f3cd026f4abdc0331c (diff)
Merge PR #11497: [opam] Don't disable native compute in opam.dev file
Reviewed-by: SkySkimmer
-rw-r--r--coq.opam2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq.opam b/coq.opam
index 50f746abec..39191c21d9 100644
--- a/coq.opam
+++ b/coq.opam
@@ -28,7 +28,7 @@ depends: [
]
build: [
- [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
+ [ "./configure" "-prefix" prefix ]
[ "make" "-f" "Makefile.dune" "voboot" ]
[ "dune" "build" "-p" name "-j" jobs ]
]