Ticket #22182: patch-Portfile.diff

File patch-Portfile.diff, 679 bytes (added by kiyoshi.coquser@…, 15 years ago)

  • Portfile

    old new  
    3333build.target       world
    3434destroot.target    install
    3535destroot.destdir   COQINSTALLPREFIX=${destroot}
    36 patchfiles         patch-doc-tools-latex_filter.diff
    3736
    3837post-activate   { ui_msg "The style file for LaTeX documentation,"
    3938                  ui_msg "coqdoc.sty, is in ${prefix}/share/coq/latex."
    … …  
    4746                                       port:netpbm
    4847                  configure.args-delete -with-doc no
    4948                  configure.args-append -with-doc yes
     49                  use_parallel_build no
    5050}
    5151
    5252variant coqide description {Install CoqIDE} {