aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-08 17:13:49 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-08 17:17:15 +0100
commitaab9a48b16ffbc6b697da39d314298b692447b72 (patch)
tree395e20725b72ccdcd0f155dd4b27a251f6e63ae6 /configure.ml
parent8cefdd3289776ed58199e5f608802546d6681eef (diff)
pre-commit: nicer messages
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions