summaryrefslogtreecommitdiff
path: root/debian
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:28:00 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 15:41:39 +0200
commitdbb8a5704033fb6990af449e29c6018286d4b044 (patch)
tree632587404f51d58e6600c8920c17ae4f260f58ca /debian
parent38db629f4be6f0a963b95a958a99bbe382b6b5d1 (diff)
Disable compiling/installing doc
Diffstat (limited to 'debian')
-rwxr-xr-xdebian/rules3
1 files changed, 2 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules
index cd34b8bc..8075e719 100755
--- a/debian/rules
+++ b/debian/rules
@@ -17,7 +17,8 @@ OCAMLABI := $(shell ocamlc -version)
CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \
--emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all \
- --browser "/usr/bin/x-www-browser %s &"
+ --browser "/usr/bin/x-www-browser %s &" \
+ --with-doc no
configure: configure-stamp
configure-stamp: