0
0
mirror of https://github.com/mongodb/mongo.git synced 2024-11-22 04:59:34 +01:00
mongodb/evergreen/functions/download_pgo_profile.sh
Daniel Hill bf6744de88 SERVER-93201: add PGO (#25342)
GitOrigin-RevId: 2312148c761d206dcc0404824579ee8586225f77
2024-08-07 12:48:52 +00:00

15 lines
263 B
Bash
Executable File

DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" > /dev/null 2>&1 && pwd)"
. "$DIR/../prelude.sh"
set +o errexit
cd src
if [ -z "${PGO_PROFILE_URL:-}" ]; then
echo "No pgo profile url specified" >&2
exit 0
fi
wget $PGO_PROFILE_URL
tar -xvf default.profdata.tgz