0
0
mirror of https://github.com/mongodb/mongo.git synced 2024-11-24 00:17:37 +01:00
mongodb/evergreen/record_mongodb_server_version.sh
Trevor 950acfb704 SERVER-85798 fix build_patch_id (#18439)
GitOrigin-RevId: cbec817baa0eea96d060f78836ddd6fbb9a07c41
2024-01-27 02:47:21 +00:00

15 lines
258 B
Bash
Executable File

DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" > /dev/null 2>&1 && pwd)"
. "$DIR/prelude.sh"
cd src
set -o errexit
set -o verbose
build_patch_id="${build_patch_id:-${reuse_compile_from}}"
if [ -n "${build_patch_id}" ]; then
exit 0
fi
"$1" --version > "$2"