From 0557d9cf49360cef6727e70e5f876fcbf15b1165 Mon Sep 17 00:00:00 2001 From: Giang Nguyen Date: Tue, 20 Aug 2024 19:45:42 +0200 Subject: [PATCH] Fix build file --- build_third_parties.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/build_third_parties.sh b/build_third_parties.sh index 8a47c812..04b881a1 100755 --- a/build_third_parties.sh +++ b/build_third_parties.sh @@ -139,6 +139,7 @@ if [ $BUILD_MUJOCO = true ]; then FROM_SRC=false MUJOCO_BUILD_DIR=$BUILD_DIR/mujoco + MUJOCO_EXT_DIR=$EXT_DIR/mujoco if [ ! -d "$MUJOCO_BUILD_DIR" ]; then # Create the folder if it doesn't exist