mirror of
https://github.com/github/gitignore.git
synced 2026-10-25 12:12:23 +01:00
Merge pull request #2807 from lorenzleutgeb/patch-1
Create HOL.gitignore
This commit is contained in:
1 file changed
+11
@@ -0,0 +1,11 @@
|
|||||||
|
*Script
|
||||||
|
|
||||||
|
# Holmake generated files
|
||||||
|
*Theory.sig
|
||||||
|
*Theory.sml
|
||||||
|
*.uo
|
||||||
|
*.ui
|
||||||
|
|
||||||
|
# Holmake auxiliary files
|
||||||
|
.hollogs
|
||||||
|
.HOLMK
|
||||||
Reference in new issue
Block a user