diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 16:34:46 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-04 16:34:46 +0100 |
commit | f637fa599b6b7226d131738cf5db61fd694cb479 (patch) | |
tree | 3de5bbe8f7006e91308d38bed22fb30200c4fc9e /toplevel/coqtop.ml | |
parent | 97f4f3cc0425b62b1e23454dca85a10eea605ef5 (diff) | |
parent | 2d8da3841c3a34666d164cd944e936c56dcf4a23 (diff) |
Merge PR #6882: Harden gitattributes against core.whitespace configuration.
Diffstat (limited to 'toplevel/coqtop.ml')
0 files changed, 0 insertions, 0 deletions