diff options
| author | Alasdair Armstrong | 2017-10-25 15:50:58 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-10-25 15:50:58 +0100 |
| commit | 4cbcf71c54628b13e6ced99b4c9ce1edbd1bffe1 (patch) | |
| tree | 300757aeddde980cd641fd3d39240b0279683907 /.gitignore | |
| parent | be87b5725853038123f2d6b5a04eb159a46f865c (diff) | |
Point sail/src makefile at ott file in language/
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -1,3 +1,4 @@ +*~ *.native *.byte src/_build/ |