Ticket #22292: patch-Makefile.doc.diff

File patch-Makefile.doc.diff, 633 bytes (added by kiyoshi.coquser@…, 15 years ago)

  • Makefile.doc

    old new  
    193193        $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
    194194          -R theories Coq $(THEORIESVO:.vo=.v)
    195195        mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
     196        -$(INSTALLLIB) tools/coqdoc/coqdoc.css doc/stdlib/html
    196197
    197198doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
    198199        ./doc/stdlib/make-library-index doc/stdlib/index-list.html