File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 11#! /bin/bash
2+ set -euo pipefail
23
3- source ./safeCommandsSet.sh
4+ if (git submodule status 2>&1 || true) | grep -iq " fatal: Not a git repository (or any of the parent directories): .git" ; then
5+ pushd " $( dirname " $0 " ) " /../external/
46
5- if git submodule status 2>&1 | grep -iq " fatal: Not a git repository (or any of the parent directories): .git" ; then
7+ git clone --no-checkout https://github.com/nlohmann/json.git
8+ pushd json/
9+ git checkout v3.12.0
10+ popd
611
7- safe_cd " $( dirname " $0 " ) " /../external/
12+ git clone --no-checkout https://github.com/pboettch/json-schema-validator.git
13+ pushd json-schema-validator/
14+ git checkout 2.3.0
15+ popd
816
9- git clone --no-checkout https://github.com/nlohmann/json.git
10- safe_cd json/
11- git checkout v3.11.3
12- safe_cd -
13-
14- git clone --no-checkout https://github.com/pboettch/json-schema-validator.git
15- safe_cd json/
16- git checkout 2.3.0
17- safe_cd -
18-
19- else git submodule update --init;
17+ popd
18+ else
19+ git submodule update --init;
2020fi
You can’t perform that action at this time.
0 commit comments