summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorBrian Campbell2018-04-13 15:18:21 +0100
committerBrian Campbell2018-04-13 15:18:21 +0100
commit4cabe141fc5f89627fcb44f6c90b24daedc70c89 (patch)
tree3a62a74c4c0c1434f54250dbbe7734595124db9e /.gitignore
parent2e44dbdaccfd39e18a451a5403ebac89aa34ac09 (diff)
Add a few more generated file to gitignore
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore5
1 files changed, 5 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 87e0cdfd..7c36889b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,13 @@
+/sail
*~
*.native
*.byte
src/_build/
src/sail.docdir
+src/ast.lem
+src/ast.ml
+src/bytecode.lem
+src/bytecode.ml
_sbuild/
test/typecheck/rtpass*/
language/*.pdf