equal
deleted
inserted
replaced
20 ## Pure |
20 ## Pure |
21 |
21 |
22 BOOTSTRAP_FILES = \ |
22 BOOTSTRAP_FILES = \ |
23 General/exn.ML \ |
23 General/exn.ML \ |
24 General/timing.ML \ |
24 General/timing.ML \ |
25 ML-Systems/bash.ML \ |
|
26 ML-Systems/compiler_polyml-5.2.ML \ |
25 ML-Systems/compiler_polyml-5.2.ML \ |
27 ML-Systems/compiler_polyml-5.3.ML \ |
26 ML-Systems/compiler_polyml-5.3.ML \ |
28 ML-Systems/ml_name_space.ML \ |
27 ML-Systems/ml_name_space.ML \ |
29 ML-Systems/ml_pretty.ML \ |
28 ML-Systems/ml_pretty.ML \ |
30 ML-Systems/multithreading.ML \ |
29 ML-Systems/multithreading.ML \ |
53 |
52 |
54 |
53 |
55 Pure: $(OUT)/Pure |
54 Pure: $(OUT)/Pure |
56 |
55 |
57 $(OUT)/Pure: $(BOOTSTRAP_FILES) \ |
56 $(OUT)/Pure: $(BOOTSTRAP_FILES) \ |
|
57 Concurrent/bash.ML \ |
|
58 Concurrent/bash_sequential.ML \ |
58 Concurrent/cache.ML \ |
59 Concurrent/cache.ML \ |
59 Concurrent/future.ML \ |
60 Concurrent/future.ML \ |
60 Concurrent/lazy.ML \ |
61 Concurrent/lazy.ML \ |
61 Concurrent/lazy_sequential.ML \ |
62 Concurrent/lazy_sequential.ML \ |
62 Concurrent/mailbox.ML \ |
63 Concurrent/mailbox.ML \ |