diff --git a/resource-1.0/Makefile b/resource-1.0/Makefile index 9fb83211c..33e33764b 100644 --- a/resource-1.0/Makefile +++ b/resource-1.0/Makefile @@ -19,7 +19,7 @@ langs: present: chmod u+x mkPresent - $(GF) -make -src -preproc=./mkPresent */Lang??*.gf + $(GF) -make -src -preproc=./mkPresent */Lang??*.gf +RTS -M800M -K100M mv */*.gfc */*.gfr ../present mathematical: