Deal with recentbashisms

.gitlab-ci.yml

@@ -7,10 +7,8 @@ default:
 build:
   script:
     - apk --no-cache add make git
-    - pandoc --version
-    - git --version
-    - git branch --verbose
-    - git branch --verbose --remote
+    - sh --version; git --version; pandoc --version
+    - git branch --verbose; git branch --verbose --remote
     - make prepare wipe
     - make
     - make publish

Makefile

@@ -16,10 +16,10 @@ all : $(OUT_MARKUP) $(OUT_OTHERS)
 prepare : $(OUT)
 	git fetch origin public
 	git worktree add $(OUT) public
-	if [[ -v DEPLOY_TOKEN ]]; then \
-		git config user.name  "$GITLAB_USER_NAME"; \
-		git config user.email "$GITLAB_USER_EMAIL"; \
-		git remote set-url origin "https://cicd:${DEPLOY_TOKEN}@${CI_SERVER_HOST}/${CI_PROJECT_PATH}.git"; \
+	if [ -n "$${DEPLOY_TOKEN}" ]; then \
+		git config user.name  '${GITLAB_USER_NAME}'; \
+		git config user.email '${GITLAB_USER_EMAIL}'; \
+		git remote set-url origin "https://cicd:$${DEPLOY_TOKEN}@${CI_SERVER_HOST}/${CI_PROJECT_PATH}.git"; \
 	fi
 
 wipe :
@@ -28,7 +28,7 @@ wipe :
 publish :
 	git -C $(OUT) add .
 	git -C $(OUT) commit --message 'Publish from $(shell git rev-parse HEAD)'
-	git -C $(OUT) push --push-option ci.skip origin HEAD:public
+	git -C $(OUT) push --push-option ci.skip origin 'HEAD:public'
 
 clean :
 	rm -fr $(OUT)