diff --git a/.gitignore b/.gitignore index 18ffffcbd..b22cc36f4 100644 --- a/.gitignore +++ b/.gitignore @@ -37,6 +37,11 @@ dune-project *~ \#*\# +[._]*.s[a-v][a-z] +[._]*.sw[a-p] +[._]s[a-rt-v][a-z] +[._]ss[a-gi-z] +[._]sw[a-p] *.rej *.orig