build: Do not fail when '.git' is missing.

This is a followup to a5d719012e.

* Makefile.am (.git/hooks/pre-push): Add dash.
This commit is contained in:
Ludovic Courtès 2023-05-04 18:49:58 +02:00
parent d0a6c11079
commit 5aa1f3aa4a
No known key found for this signature in database
GPG key ID: 090B11993D9AEBB5

View file

@ -1115,7 +1115,7 @@ cuirass-jobs: $(GOBJECTS)
# Git auto-configuration.
.git/hooks/pre-push: etc/git/pre-push
cp etc/git/pre-push .git/hooks/pre-push
-cp etc/git/pre-push .git/hooks/pre-push
.git/config: etc/git/gitconfig
-git config include.path ../etc/git/gitconfig