author | paulson |
Tue, 29 Aug 2017 17:41:27 +0100 | |
changeset 66553 | 6ab32ffb2bdd |
parent 39448 | 64639ff50fcd |
permissions | -rw-r--r-- |
39433
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
1 |
include Makefile |
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
2 |
bin/mosml/Makefile.src: |
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
3 |
mkdir -p `dirname $@` |
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
4 |
echo > $@ |
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
5 |
refresh_FILES: |
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
6 |
echo $(POLYML_SRC) | \ |
39448 | 7 |
sed "s/src\/PortablePolyml/PortableIsabelle/g" | \ |
8 |
sed "s/ src\/Tptp\.s[a-z][a-z]//g" | \ |
|
9 |
sed "s/ src\/Options\.s[a-z][a-z]//g" \ |
|
39433
3e41c9d29769
make "metis.ML" building process slightly more robust by eliminating the need for "FILES";
blanchet
parents:
diff
changeset
|
10 |
> FILES |