Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-01-24 14:45:23 -0800 (Thu, 24 Jan 2008)
Revision: 12699
Log message:

      Minor changes needed to compile with OMake 0.9.8.x.
     
     This default rule is causing problems:
     
     #
     # XXX: JYH: disable this for now.  It is getting applied in too
     # many places.
     #
     %.cmx %.o: %.ml disable-this-rule
        @echo $(quote *** Error: MetaPRL file $(in $(ROOT), $(file $<)) $'does not have
     ***        a corresponding' $(in $(ROOT), $(file $*.mli)))
        exit 1

Changes  Path(relative to metaprl)
+5 -1 OMakefile_theories
+1 -1 OMakeroot
+1 -1 editor/ml/OMakefile
+1 -0 support/display/OMakefile