diff options
| author | Gaëtan Gilbert | 2020-02-03 14:52:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-03 14:52:20 +0100 |
| commit | 1c1c04d0e3e02ce461fb953f08e2d8c68e52ee63 (patch) | |
| tree | 655aa6765cdba78618a3f9bf7523237ac31846dc | |
| parent | 45f0dc36a749371de35a5d4b998e1305f47e3beb (diff) | |
| parent | b35030760cadd96a968e04f3cd026f4abdc0331c (diff) | |
Merge PR #11497: [opam] Don't disable native compute in opam.dev file
Reviewed-by: SkySkimmer
| -rw-r--r-- | coq.opam | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 ] ] |
