aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik.martin-dorel@irit.fr>2016-10-16 00:02:39 +0200
committerGravatar Erik Martin-Dorel <erik.martin-dorel@irit.fr>2016-10-16 00:04:51 +0200
commit25355560b4aa25b17b754c33c9ba2a18d7498df4 (patch)
tree318f6a735d546232aef6ddb3644941924c139538 /.gitignore
parenta51f0da56e93ff5c892d6de4f9b46483ffc6b383 (diff)
Update CHANGES.
Related: ProofGeneral/PG#41
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions