equal
deleted
inserted
replaced
|
1 include Makefile |
|
2 bin/mosml/Makefile.src: |
|
3 mkdir -p `dirname $@` |
|
4 echo > $@ |
|
5 refresh_FILES: |
|
6 echo $(POLYML_SRC) | \ |
|
7 sed "s/src\///g" | \ |
|
8 sed "s/ Tptp\.s[a-z][a-z]//g" | \ |
|
9 sed "s/ Options\.s[a-z][a-z]//g" \ |
|
10 > FILES |