equal
deleted
inserted
replaced
30 ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \ |
30 ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \ |
31 ML-Systems/polyml.ML ML-Systems/polyml_common.ML \ |
31 ML-Systems/polyml.ML ML-Systems/polyml_common.ML \ |
32 ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ |
32 ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \ |
33 ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ |
33 ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \ |
34 ML-Systems/timing.ML ML-Systems/time_limit.ML \ |
34 ML-Systems/timing.ML ML-Systems/time_limit.ML \ |
35 ML-Systems/universal.ML |
35 ML-Systems/universal.ML ML-Systems/unsynchronized.ML |
36 |
36 |
37 RAW: $(OUT)/RAW |
37 RAW: $(OUT)/RAW |
38 |
38 |
39 $(OUT)/RAW: $(BOOTSTRAP_FILES) |
39 $(OUT)/RAW: $(BOOTSTRAP_FILES) |
40 @./mk -r |
40 @./mk -r |