aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2016-01-21 22:17:36 +0100
committerMaxime Dénès2016-01-21 22:17:36 +0100
commitaa1913411547eeed464b024f1cf54113be26e929 (patch)
tree5f7dcc1d69b0fb04f9e6ee9a8d022ed0e181ba28 /dev
parent5e23fb90b39dfa014ae5c4fb46eb713cca09dbff (diff)
Compile OS X binaries without native_compute support.
Diffstat (limited to 'dev')
-rwxr-xr-xdev/make-macos-dmg.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 70889badc1..20b7b5b531 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -8,7 +8,7 @@ eval `opam config env`
make distclean
OUTDIR=$PWD/_install
DMGDIR=$PWD/_dmg
-./configure -debug -prefix $OUTDIR
+./configure -debug -prefix $OUTDIR -native-compiler no
VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
APP=bin/CoqIDE_${VERSION}.app