index
:
terralloc.git
master
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
terralloc
blob: 386e9fc06a8eb0a89d94237e2b1923caa8a20f1f (
plain
) (
blame
)
1
2
3
#!/bin/bash dist/build/final/final +RTS -K3000000000 -RTS $@