projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 901c251) | patch
Rename git-whitespace-hook to dune-git-whitespace-hook.
authorAnsgar Burchardt <ansgar@debian.org>
Thu, 21 Jun 2018 07:17:17 +0000 (08:17 +0100)
committerAnsgar Burchardt <ansgar@debian.org>
Thu, 21 Jun 2018 07:17:17 +0000 (08:17 +0100)
commit5d95d322327be59d6ed43177f86c49644f544d7c
tree33534982f6c70e45d0c6fe04429076bffc9a4ebatree | snapshot
parent901c25160930d4eb258f4432c8ff570ae9bde642commit | diff
Rename git-whitespace-hook to dune-git-whitespace-hook.

The name git-whitespace-hook is a bit too generic for a DUNE-specific
tool.

Gbp-Pq: Name rename-git-whitespace-hook.patch
bin/dunecontrol diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.