diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 16:48:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 16:48:51 +0200 |
| commit | a88339e768ad1c3c36250dff659120236b900cf0 (patch) | |
| tree | ad1d5315a69218dc52403cc89d25d26f3236d17b | |
| parent | ad9b0fc2f2c0945eb48ae6d9cd7256b11dfd8792 (diff) | |
glob.dump is not there anymore
| -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 |