diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:28:00 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 15:41:39 +0200 |
| commit | dbb8a5704033fb6990af449e29c6018286d4b044 (patch) | |
| tree | 632587404f51d58e6600c8920c17ae4f260f58ca /debian | |
| parent | 38db629f4be6f0a963b95a958a99bbe382b6b5d1 (diff) | |
Disable compiling/installing doc
Diffstat (limited to 'debian')
| -rwxr-xr-x | debian/rules | 3 |
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: |