diff options
Diffstat (limited to 'Makefiledefault')
| -rw-r--r-- | Makefiledefault | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefiledefault b/Makefiledefault new file mode 100644 index 000000000000..9d7925152194 --- /dev/null +++ b/Makefiledefault @@ -0,0 +1,6 @@ +ifeq ($(MLCOMP)x,x) +MLCOMP=mlton @MLton ram-slop 0.7 -- -disable-pass deepFlatten -disable-pass refFlatten +#mlton @MLton ram-slop 0.7 gc-summary -- -disable-pass deepFlatten -verbose 3 +endif + +export MLCOMP |