From b35030760cadd96a968e04f3cd026f4abdc0331c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Jan 2020 16:17:32 +0100 Subject: [opam] Don't disable native compute in opam.dev file See discussion in https://github.com/coq/bignums/issues/26 and #11476 We still disable it in developer fast builds as the speed up is considerable, it can be enabled by just calling `./configure` --- coq.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ] ] -- cgit v1.2.3