aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-13 13:42:04 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-13 13:44:10 +0200
commit0e94cb62410354e5df4e65b34e7cbf8451b31d6e (patch)
treee50d291966da1ad791458a3ceea6d827857d5852 /.gitignore
parent93ae6db3375d442ef67154c832bbdf155cffe32f (diff)
Fixing #5078 (wrong detection of evaluable local hypotheses).
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions