diff options
| author | Gabriel Kerneis | 2013-10-04 16:22:10 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2013-10-04 16:22:36 +0100 |
| commit | 59743ba08d0f3a3237b5316a7395ead732199ed8 (patch) | |
| tree | c38b9064c89f82f0151b21312b95b04d1a10a6aa /.gitignore | |
| parent | 9934af065d693b76b8a67879f042145296b29813 (diff) | |
Clean up build system
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 17 |
1 files changed, 16 insertions, 1 deletions
@@ -1 +1,16 @@ -src/_build/* +*.native +*.byte +src/_build/ +src/lem_interp/_build/ +src/lem_interp/*.ml +language/*.pdf +language/*.uo +language/*.ui +language/*.sig +language/*.sml +language/.HOLMK +language/*.tex +language/*.aux +language/*.log +language/*.dvi +language/*.ps |