>>>>> "Michael" == Michael Roth <mroth at nessie.de> writes: Michael> The current /binaries/* hid the directory, but completely removed Michael> it by "git-clean -d", which should not be intended. Applied, thanks. -- Bye, Peter Korsgaard