aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-06-24 13:35:02 +0200
committerGaëtan Gilbert2020-06-24 13:35:02 +0200
commite22a74188414de6b1f005b98c49c0be17d78cbbd (patch)
treee464d83e04f46b1a0d3d05d87f183a384dc772fe
parent3ba88c944db09003caaa668699230613b1bca793 (diff)
Revert "[opam] Don't disable native compute in opam.dev file"
This reverts commit b35030760cadd96a968e04f3cd026f4abdc0331c.
-rw-r--r--coq.opam2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq.opam b/coq.opam
index e46f9def60..23cef68dce 100644
--- a/coq.opam
+++ b/coq.opam
@@ -28,6 +28,6 @@ depends: [
]
build: [
- [ "./configure" "-prefix" prefix ]
+ [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
[ "dune" "build" "-p" name "-j" jobs ]
]