mirror of
https://github.com/github/gitignore
synced 2024-11-26 05:34:21 +01:00
Create HOL.gitignore
This commit is contained in:
parent
28222daa1e
commit
6f8210fe16
11
HOL.gitignore
Normal file
11
HOL.gitignore
Normal file
@ -0,0 +1,11 @@
|
|||||||
|
*Script
|
||||||
|
|
||||||
|
# Holmake generated files
|
||||||
|
*Theory.sig
|
||||||
|
*Theory.sml
|
||||||
|
*.uo
|
||||||
|
*.ui
|
||||||
|
|
||||||
|
# Holmake auxiliary files
|
||||||
|
.hollogs
|
||||||
|
.HOLMK
|
Loading…
Reference in New Issue
Block a user