Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-10-22 20:35:14 -0700 (Wed, 22 Oct 2003)
Revision: 5030
Log message:

      - Adding a "doc" target that would build all the files that are
      currently posted on the web (note: some of the "omake tex" files
      require Lucida fonts, but "omake doc" should work without them).
      
      - Added htmldoc html->ps/pdf converter to omake and added the
      htmldoc-generated files to "omake doc"
      
      - make will now print a warning message telling people that
      using make is no longer recommended and that omake should
      be used instead.
      

Changes	Path
+7 -2	metaprl/Makefile
+2 -2	metaprl/OMakefile
Added	metaprl/doc/Files
Properties	metaprl/doc/Files
+1 -47	metaprl/doc/Makefile
Added	metaprl/doc/OMakefile
Properties	metaprl/doc/OMakefile
+1 -1	metaprl/doc/latex/theories/OMakefile
+4 -3	metaprl/doc/ps/theories/OMakefile