prepare an archive independent from autoconf

ybertot · Sep 14, 2017 · 7a0bb4f · 7a0bb4f
1 parent 7ab2982
commit 7a0bb4f
Show file tree

Hide file tree

Showing 3 changed files with 3,566 additions and 229 deletions.
diff --git a/.gitignore b/.gitignore
@@ -12,7 +12,6 @@
 version.ml
 
 autom4te.cache
-configure
 Makefile
 config.log
 config.status