aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-06 12:47:22 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-06 12:47:22 +0200
commitf1598b00219a951e94036cb7f48a8fe1309025f1 (patch)
tree62dd9a6da381137e61a6b732ae0ba806d822c5cc /configure.ml
parent6cb1829829de5edfe733b901c38a8b39ba03ef56 (diff)
parent248fffe64ee42137822ba438dfb378defbe1aa05 (diff)
Merge PR #1127: Shorten the .gitattributes file.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions