diff options
Diffstat (limited to 'debian')
| -rwxr-xr-x | debian/rules | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/debian/rules b/debian/rules index e50ad147..50a6e64f 100755 --- a/debian/rules +++ b/debian/rules @@ -50,11 +50,6 @@ build-stamp: configure-stamp else \ $(MAKE) BEST=byte HASCOQIDE=byte check; \ fi - if [ -e opt-stamp ]; then \ - $(MAKE) BEST=opt glob.dump; \ - else \ - $(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \ - fi cp tools/coqdoc/coqdoc.sty doc/stdlib/ $(MAKE) -f Makefile.stage3 doc/stdlib/html/index.html COQDOC="bin/coqdoc --coqlib_path `pwd`" touch build-stamp |