Skip to content

#1288 Version control setup command in dunecontrol and installation of whitespace hook

Metadata

Property Value
Reported by Steffen Müthing (steffen.muething@iwr.uni-heidelberg.de)
Reported at Apr 29, 2013 13:44
Type Feature Request
Version Git (pre2.4) [autotools]
Operating System Unspecified / All
Last edited by Carsten Gräser (graeser@math.fu-berlin.de)
Last edited at Sep 3, 2013 11:57
Closed by Carsten Gräser (graeser@math.fu-berlin.de)
Closed at Sep 3, 2013 11:57
Closed in version 2.3
Resolution Fixed
Comment Fix by Steffen Müthing is pushed.

Description

Before we can switch the repositories to Git, we have to solve the issue of distributing and installing a local whitespace enforcing hook in cloned repositories. Otherwise, people will forget to do so and we get lots of rejected merges.

Unfortunately, Git does not support cloning whitespace hooks for security reasons (portability might be an issue as well). After discussing the problem with Christian, we settled on adding a new version control setup command in dunecontrol that will automatically be called as part of "dunecontrol all". As some repositories might require additional custom setup procedures, the command can also be extended by scripts distributed as part of the repository.

Here's the breakdown of the patch series:

0001 adds the Git whitespace pre-commit hook to dune-common. This file will be installed using the new dunecontrol command.

0002 adds the new command called vcsetup. See the commit message at the top of the patch file for further details about its features and the way it works, but as a module author, you are probably fine with knowing that you can have the whitespace hook installed for your module by adding the line "Whitespace-Hook: Yes" to you dune.module file.

0003 hooks vcsetup into the "dunecontrol all" sequence to make sure it gets run by everyone who is following our standard building instructions.

0004 turns on installation of the whitespace hook for dune-common itself.

0005 is an optional extension that allows the user to supply a number of custom settings for the Git repository. An example of why this might be useful: By default, I use my standard email address for my Git identity, but for the Dune modules, I want to switch to my @dune-project.org alias. By integrating this customization into my options file, I can be sure that I will not forget it when cloning repositories.

Any comments, suggestions, problems with the implementation? If not, could someone please apply the patches? Thanks!

Attachments