init du répertoire séparé

Arthur-Milchior · Sep 16, 2014 · ddc294e · ddc294e
commit ddc294e
Show file tree

Hide file tree

Showing 42 changed files with 7,221 additions and 0 deletions.
diff --git a/_tags b/_tags
@@ -0,0 +1,2 @@
+<*>: pkg_batteries,batteries.pa_string.syntax,pkg_threads
+true: use_menhir,use-ocamlfind,debug
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		<*>: pkg_batteries,batteries.pa_string.syntax,pkg_threads
		true: use_menhir,use-ocamlfind,debug