Merge 6328a8da94 into 24b539acec

Create HOL.gitignore

Global/OhMyOpenAgent.gitignore

@@ -0,0 +1,2 @@
+.sisyphus/*
+!.sisyphus/rules/

README.md

@@ -57,7 +57,7 @@ Include details when opening pull request if the template is important and visib
 may not accept it immediately, but we can promote it to the root at a later date
 based on interest.
 
-Please also understand that we can’t list every tool that ever existed.
+Please also understand that we can’t list every tool that has ever existed.
 Our aim is to curate a collection of the _most common and helpful_ templates,
 not to make sure we cover every project possible. If we choose not to
 include your language, tool, or project, it’s not because it’s not awesome.

community/HOL.gitignore

@@ -0,0 +1,11 @@
+*Script
+
+# Holmake generated files
+*Theory.sig
+*Theory.sml
+*.uo
+*.ui
+
+# Holmake auxiliary files
+.hollogs
+.HOLMK