summaryrefslogtreecommitdiff
path: root/debian/rules
diff options
context:
space:
mode:
Diffstat (limited to 'debian/rules')
-rwxr-xr-xdebian/rules1
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules
index dd9cf72c..c12c540d 100755
--- a/debian/rules
+++ b/debian/rules
@@ -38,7 +38,6 @@ CONFIGUREOPTS := -arch Linux -prefix /usr -mandir /usr/share/man \
-browser "/usr/bin/x-www-browser %s &" \
-coqide no \
-with-doc no \
- -debug \
$(NATIVE_COMPUTE)
export OCAMLINIT_SED += \