diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 18:54:46 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 18:54:46 +0100 |
commit | 2f13806f10b2781f84417014c8018097c8e8b2ad (patch) | |
tree | bda1e7175976e5f695f058e967cc3a2b60456745 /plugins/extraction/g_extraction.ml4 | |
parent | 8669a9449a11cc2e5ddeeba5b0ddc44c7a978d44 (diff) | |
parent | aab9a48b16ffbc6b697da39d314298b692447b72 (diff) |
Merge PR #6283: A pre-commit hook to magically fix whitespace issues.
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
0 files changed, 0 insertions, 0 deletions