diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-10-05 15:29:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-10-05 15:29:41 +0200 |
| commit | 248fffe64ee42137822ba438dfb378defbe1aa05 (patch) | |
| tree | 6eb25b6e7211058d870e5920f0159a37e622e6a6 /vernac/metasyntax.ml | |
| parent | 8b5f7ad0722e5ed1b87589ae103a1c4c5974416f (diff) | |
Shorten the .gitattributes file.
.dir-locals.el can be useful for users of the tarballs as well,
and TODO doesn't exist anymore.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions