diff options
130 files changed, 3620 insertions, 12528 deletions
diff --git a/.gitignore b/.gitignore index 8178a2214b..0772abe3ce 100644 --- a/.gitignore +++ b/.gitignore @@ -10,7 +10,7 @@ /.dir-locals.el # Top level excludes -/Makefile.bak +/Makefile.orig /Makefile /MINFO /TABLE @@ -22,6 +22,8 @@ /out.* /tmp.* +**/Makefile + /test/*.ss /test/*.srl /test/.rnd |