diff options
Diffstat (limited to 'src/editor/simple/Makefile')
| -rw-r--r-- | src/editor/simple/Makefile | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/editor/simple/Makefile b/src/editor/simple/Makefile deleted file mode 100644 index 00a97b337..000000000 --- a/src/editor/simple/Makefile +++ /dev/null @@ -1,7 +0,0 @@ - -save: save.hs - ghc --make save.hs - -install:: - @make save - rsync -avz --exclude .DS_Store P *.html *.css *.js ../../runtime/javascript/minibar/support.js *.cgi *.manifest save www.grammaticalframework.org:/usr/local/www/GF/demos/gfse |