diff options
Diffstat (limited to 'debian/rules')
-rwxr-xr-x | debian/rules | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index 7f7b8051..5083fdf8 100755 --- a/debian/rules +++ b/debian/rules @@ -34,7 +34,6 @@ endif CONFIGUREOPTS := -arch Linux -prefix /usr -mandir /usr/share/man \ -configdir /etc/xdg/coq \ - -emacslib /usr/share/emacs/site-lisp/coq \ -browser "/usr/bin/x-www-browser %s &" \ -coqide no \ -with-doc no \ |