diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-07-28 16:02:40 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-07-28 16:08:21 +0200 |
| commit | d6c7661cea5a874663179d806199634b7c4076ed (patch) | |
| tree | 4a4a1a967a8261f85be14ec4b73b24954192a117 /debian/rules | |
| parent | 10a7bc14dc87b57b022facbbbf3b31d74a4445e5 (diff) | |
Fix building of (stdlib) doc
Diffstat (limited to 'debian/rules')
| -rwxr-xr-x | debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index a9bd3b67..5151c911 100755 --- a/debian/rules +++ b/debian/rules @@ -51,7 +51,7 @@ build-stamp: patch-stamp configure-stamp $(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \ fi cp tools/coqdoc/coqdoc.sty doc/stdlib/ - $(MAKE) -C doc stdlib/html/index.html + $(MAKE) -f Makefile.stage3 doc/stdlib/html/index.html COQDOC="bin/coqdoc --coqlib_path `pwd`" touch build-stamp clean: unpatch |