diff options
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -8,3 +8,4 @@ literature.pdf | |||
8 | **.log | 8 | **.log |
9 | **.prof | 9 | **.prof |
10 | **.prof.* | 10 | **.prof.* |
11 | examples | ||
index : incremental-dfsts | ||
[no description] | gkleen |
summaryrefslogtreecommitdiff |