From 6c15ead6c96aaaccf13b1445de2e7570ec5fe218 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 11 Aug 2021 19:50:56 +0200 Subject: [PATCH] docs: last-minute improvements (#62) * docs(README.md): Fix details * docs: s/docker-coq/docker/ as docker-coq-action is not coq-specific --- README.md | 10 +++++----- entrypoint.sh | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index ff6e318..e70e8f7 100644 --- a/README.md +++ b/README.md @@ -444,7 +444,7 @@ endGroup Beware that the following script is *buggy*: -```bash +```yaml script: | startGroup "Build project" make -j2 && make test && make install @@ -453,7 +453,7 @@ script: | Because if `make test` fails, it won't make the CI fail. -
Explanation +
(Explanation) This is a typical pitfall that occur *in any shell-based CI platform* where the [`set -e`]( @@ -481,7 +481,7 @@ Instead, you should write one of the following variants: * using semicolons: - ```bash + ```yaml script: | startGroup "Build project" make -j2 ; make test ; make install @@ -490,7 +490,7 @@ Instead, you should write one of the following variants: * using newlines: - ```bash + ```yaml script: | startGroup "Build project" make -j2 @@ -501,7 +501,7 @@ Instead, you should write one of the following variants: * using `&&` but within a subshell: - ```bash + ```yaml script: | startGroup "Build project" ( make -j2 && make test && make install ) diff --git a/entrypoint.sh b/entrypoint.sh index 5260fcf..03bf45c 100755 --- a/entrypoint.sh +++ b/entrypoint.sh @@ -160,7 +160,7 @@ if test -z "$INPUT_CUSTOM_SCRIPT_EXPANDED"; then exit 1 fi -startGroup "Pull docker-coq image" +startGroup "Pull docker image" echo COQ_IMAGE="$COQ_IMAGE" docker pull "$COQ_IMAGE"