update .gitignore for src/config/

84775168 · Andrei Paskevich · df6d3b7c · 84775168
Commit 84775168 authored Oct 29, 2010 by Andrei Paskevich
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

.gitignore .gitignore +4 -0

No files found.
--- a/.gitignore
+++ b/.gitignore
@@ -79,6 +79,10 @@
 /src/coq-plugin/*.annot
 /src/coq-plugin/g_whytac.ml

+# /src/config/
+/src/config/*.cm*
+/src/config/*.annot
+
 # /src/core/
 /src/core/*.cm*
 /src/core/*.annot