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 |