Browse Source

Add gitignore

 - Don't track some auto-generated file
Leo 10 years ago
parent
commit
ca6082386b
1 changed files with 11 additions and 0 deletions
  1. 11 0
      .gitignore

+ 11 - 0
.gitignore

@@ -0,0 +1,11 @@
+_build
+oclaunch.byte
+session.vim
+settings_j.ml
+settings_j.mli
+settings_t.ml
+settings_t.mli
+/bin/sh: g : commande introuvable
+.paths
+.project
+.settings/