projects / dune-common.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 82acebe) | patch
Rename git-whitespace-hook to dune-git-whitespace-hook.
authorAnsgar Burchardt <ansgar@debian.org>
Sun, 18 Dec 2016 11:58:14 +0000 (11:58 +0000)
committerAnsgar Burchardt <ansgar@debian.org>
Sun, 18 Dec 2016 11:58:14 +0000 (11:58 +0000)
commite966623efde143556723d3ec4da0edd3fe1412e8
tree1b8dc46f13770abfe0097aed0a7fbc2e0579996btree | snapshot
parent82acebe32f81aac8ee045b097fe5693e1f8be6c9commit | 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.