Update server.inc

KVS85 · web-flow · commit b4b88992752a · 2025-05-10T22:35:50.000+02:00
diff --git a/jenkins/helper/server.inc b/jenkins/helper/server.inc
@@ -1,3 +1,4 @@
+if [ -z "$DOCKER" ]; then DOCKER="docker"; fi
 if [ -z "$ARANGO_AUTH" ]; then ARANGO_AUTH="auth"; fi
 if [ -z "$ARANGO_BRANCH" ]; then ARANGO_BRANCH="devel"; fi
 if [ -z "$ARANGO_DOCKER_REG" ]; then ARANGO_DOCKER_REG="docker.io/arangodb"; fi

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+if [ -z "$DOCKER" ]; then DOCKER="docker"; fi`
`1`	`2`	`if [ -z "$ARANGO_AUTH" ]; then ARANGO_AUTH="auth"; fi`
`2`	`3`	`if [ -z "$ARANGO_BRANCH" ]; then ARANGO_BRANCH="devel"; fi`
`3`	`4`	`if [ -z "$ARANGO_DOCKER_REG" ]; then ARANGO_DOCKER_REG="docker.io/arangodb"; fi`