diff -r c0eaa8b9bff5 -r 3535f16d9714 src/Tools/Metis/Makefile
--- a/src/Tools/Metis/Makefile	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/Tools/Metis/Makefile	Wed Jun 08 08:47:43 2011 +0200
@@ -22,7 +22,7 @@
   $(MLTON_TARGETS) \
   bin/mlton/*.sml bin/mlton/*.mlb \
   $(POLYML_TARGETS) \
-  bin/polyml/*.sml bin/polyml/*.o
+  bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o
 
 .PHONY: clean
 clean:
@@ -138,10 +138,12 @@
 
 METIS = bin/mlton/metis
 
+PROBLEMS2TPTP = bin/mlton/problems2tptp
+
 MLTON_TARGETS = \
   bin/mlton/selftest \
-  bin/mlton/problems2tptp \
-  $(METIS)
+  $(METIS) \
+  $(PROBLEMS2TPTP)
 
 bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
 	@$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
@@ -202,7 +204,8 @@
 	@echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
 
 bin/polyml/%.o: bin/polyml/%.sml
-	cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS)
+	cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log
+	@if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi
 
 bin/polyml/%: bin/polyml/%.o
 	@echo