diff options
| author | Ramana Kumar | 2018-05-16 16:23:01 +0100 |
|---|---|---|
| committer | Ramana Kumar | 2018-05-16 16:23:01 +0100 |
| commit | d01b227bac7c9b494e3ee5c7ac59eac3f18b697c (patch) | |
| tree | 45da55a2d74c36358e2638041d48f079fd19d07d /.gitignore | |
| parent | eee590272c8febf59d234d6f23c4e8ccd41e27dc (diff) | |
Ignore .hollogs
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -23,6 +23,7 @@ language/*.dvi language/*.ps # HOL4 .HOLMK +.hollogs *Script.sml *Theory.dat *Theory.sig |