diff options
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..b30fa842 --- /dev/null +++ b/.gitignore @@ -0,0 +1,78 @@ +*~ +.cm +src/.cm + +bin/* + +src/urweb.cm +src/urweb.mlb + +*.lex.* +*.grm.* +*.o +.deps +.libs +*.lo +*.la +*.mlton.grm +*.mlton.lex + +src/config.sml + +*.exe + +*.cache +*.log +*.status + +demo/out/*.html +demo/demo.* + +demo/more/out/*.html +demo/more/demo.* + +doc/*.html +doc/*.out + +*.sql +*mlmon.out + +*.aux +*.dvi +*.pdf +*.ps +*.toc + +.depend +Makefile.coq +*.vo +*.v.d +*.glob + +xml/parse +xml/entities.sml + +Makefile.in +src/c/Makefile.in +ar-lib +*.m4 +m4/libtool.m4 +m4/lt*.m4 +config.* +configure +depcomp +compile +install-sh +ltmain.sh +missing + +tests/*.db + +syntax: regexp + +Makefile +src/c/Makefile +libtool +include/urweb/config.h +include/urweb/config.h.in +include/urweb/stamp-h1 |