To prevent spurious trailing whitespace in the source code (which is frowned upon by the code style), a git hook checks for such whitespace automatically.

TLDR: Always run one of the following commands after cloning a core repository:

dunecontrol vcsetup # Performs setup actions related to the version control system

dunecontrol all # Complete module build, runs "dunecontrol vcsetup" as first step

The details

Lines with trailing whitespace are not allowed in the Dune source code. Unfortunately, trailing whitespace can easily creep into commits unnoticed, and not everybody uses an editor that recognizes the indentation hints. In order to keep that kind of changes out of the repositories, the server checks all pushed commits for a simplified version of the whitespace policy. Note that every version is checked, so you cannot fix a rejected commit by adding an extra commit that resolves the whitespace problem in the original commit¹.

Due to the distributed nature of Git, the server cannot check your commits as you create them in your locally cloned repository. Instead, you should install our local whitespace hook that checks every commit at creation time and immediately rejects it if there are whitespace problems. Then you can easily fix those problems, stage the additional changes and re-commit.

As Git hooks contain executable code, they are not transferred during a clone operation for security reasons, so you normally have to install hooks manually. Unfortunately, that’s just another thing to remember when cloning a repository (which tends to happen quite often with Git), so we extended dunecontrol to take care of this step for you: When you run dunecontrol all on a Dune core module, it will automatically install the most recent version of our local whitespace hook from dune-common/bin/git-whitespace-hook into that module. If you only want to install the hook without starting a complete build, you can also run

dunecontrol vcsetup # Performs setup actions related to the version control system

Footnotes