This patch allows the user to specify a file with Git configuration options that
will be applied during the vcsetup phase, which might be used to set a custom identity
within the repository (e.g. an @dune-project.org email address) or to set up personal
aliases.

In order to enable this feature, put the line
VCSETUP_FLAGS="GIT_CONFIG_FILE=</path/to/your/config/file>"
into your options file. The configuration file itself is fed to the command
"git config" line-by-line, so you can normally set an option by simply having a
line like "config_key value" in the configuration file. Lines starting with # are
skipped and can be used for comments.

[[Imported from SVN: r7470]]