Commit d4c77daa authored Jul 22, 2020 by Giacomo Bernini

upd jenkins script

parent ff376470

.jenkins.sh

100644 → 100755

+2 −0

Changes for .jenkins.sh: 2 added lines, 0 removed lines.
Original line number	Diff line number	Diff line
		@@ -11,8 +11,10 @@ rm build/*-API.json

		cd docker

		chmod +x build-container.sh
		./build-container.sh

		chmod +x run-container.sh
		./run-container.sh "${run_dir}"
		OUTCOME=$?