| author | wenzelm | 
| Fri, 16 Feb 2018 19:30:53 +0100 | |
| changeset 67631 | b7d90c4a3897 | 
| 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  |