diff options
| author | Gaëtan Gilbert | 2020-06-24 13:35:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-24 13:35:02 +0200 |
| commit | e22a74188414de6b1f005b98c49c0be17d78cbbd (patch) | |
| tree | e464d83e04f46b1a0d3d05d87f183a384dc772fe | |
| parent | 3ba88c944db09003caaa668699230613b1bca793 (diff) | |
Revert "[opam] Don't disable native compute in opam.dev file"
This reverts commit b35030760cadd96a968e04f3cd026f4abdc0331c.
| -rw-r--r-- | coq.opam | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -28,6 +28,6 @@ depends: [ ] build: [ - [ "./configure" "-prefix" prefix ] + [ "./configure" "-prefix" prefix "-native-compiler" "no" ] [ "dune" "build" "-p" name "-j" jobs ] ] |
