diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..ea759e4532452943162615c77ad455672dafa904 --- /dev/null +++ b/.gitignore @@ -0,0 +1,24 @@ +_build/ +*.res +*.native +*.byte +*.rif + +log +myocamlbuild.ml +setup.ml +setup.data +setup.log +version.tex +diff.diff +TAGS +configure +linux + +*.docdir +*.mldylib +*.mllib +linux64/ +*.cmt +Makefile.local +bin/ diff --git a/Makefile.version b/Makefile.version index 87104b20853bb7a54bb90fcfae420ef6f9776088..27a0c8b7ff5c61c66440a3e6ca8d01d7ee90c66a 100644 --- a/Makefile.version +++ b/Makefile.version @@ -3,10 +3,6 @@ SHA:=`git log -1 --pretty=format:"%h"` COMMIT_NB:=`git log --pretty=oneline | wc -l` -# until the git repo is created -SHA:=0 -COMMIT_NB:=0 - VERSION:=1.0.$(COMMIT_NB)