diff options
| author | Josh Chen | 2018-08-18 14:58:17 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 14:58:17 +0200 |
| commit | b0c85e7a4590e37d2b59d80106b993c3746445f0 (patch) | |
| tree | c95fc075c3ae57398506b9caa2163cb33cf0eca9 /.gitignore | |
| parent | bd93584da62ce4b1e43862b4119788265b00cb3c (diff) | |
.gitignore
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -2,3 +2,4 @@ *.thy~ ex/*.thy~ ex/Hott book/*.thy~ +tests/*.thy~ |