summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authoraarne <aarne@chalmers.se>2011-11-21 15:30:55 +0000
committeraarne <aarne@chalmers.se>2011-11-21 15:30:55 +0000
commit1f731df2859ad9ce2164c097b5b3f956eb87c82d (patch)
tree474ace6fdf852bc58c9c221690a64257bffd467b
parentd66110f84eec765bb26ebaa716bbce79d6c90913 (diff)
options for no-pmcfg compilation in lib/src/Make.hs (for library developers, rather than users); adding Thai to some demo and documentation
-rw-r--r--contrib/summerschool/foods/Makefile3
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/summerschool/foods/Makefile b/contrib/summerschool/foods/Makefile
index 5738bc281..8d92fe3f7 100644
--- a/contrib/summerschool/foods/Makefile
+++ b/contrib/summerschool/foods/Makefile
@@ -4,5 +4,8 @@ all:: Foods.pgf
Foods.pgf: Foods???.gf
gf -make -s -optimize-pgf Foods???.gf
+exper: Foods???.gf
+ gf -make -s -optimize-pgf Foods???.gf FoodsThai.gf
+
clean:
rm -rf *.gfo Foods.pgf