mirror of
https://github.com/mongodb/mongo.git
synced 2024-11-24 08:30:56 +01:00
fd4a98709e
GitOrigin-RevId: 1e2f6ccee4ed45be18cf04807ef253d3818095c2
16 lines
373 B
Bash
Executable File
16 lines
373 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
|
|
if [ "${use_wt_develop}" = "true" ]; then
|
|
echo "Using the wtdevelop module instead..."
|
|
cd src/third_party
|
|
for wtdir in dist examples ext lang src test tools; do
|
|
rm -rf wiredtiger/$wtdir
|
|
mv wtdevelop/$wtdir wiredtiger/
|
|
done
|
|
fi
|