Skip to content

Commit

Permalink
[CI] Fix git safe-directory on
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Apr 1, 2023
1 parent 77c76a4 commit caba457
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion .github/workflows/docker-coq.yml
Expand Up @@ -19,7 +19,9 @@ jobs:
coq_version: dev
ocaml_version: default
custom_script: |
sudo chmod -R a+rw .
sudo chmod -R a=u .
# Work around https://github.com/actions/checkout/issues/766
git config --global --add safe.directory "*"
echo '::group::install general dependencies'
sudo apt-get update -y
sudo apt-get install -y python python3
Expand Down

0 comments on commit caba457

Please sign in to comment.