--- /dev/null
+#!/usr/bin/env bash\r
+\r
+full_cmd=${BASH_SOURCE:-$0} # see http://mywiki.wooledge.org/BashFAQ/028 for a discussion of why $0 is not a good choice here\r
+dir=$(dirname "$full_cmd")\r
+cmd=${full_cmd##*/}\r
+\r
+if [ -n "$WORKSPACE" ] && [ -e "$WORKSPACE/Conf/BaseToolsCBinaries" ]\r
+then\r
+ exec "$WORKSPACE/Conf/BaseToolsCBinaries/$cmd"\r
+elif [ -n "$WORKSPACE" ] && [ -e "$EDK_TOOLS_PATH/Source/C" ]\r
+then\r
+ if [ ! -e "$EDK_TOOLS_PATH/Source/C/bin/$cmd" ]\r
+ then\r
+ echo "BaseTools C Tool binary was not found ($cmd)"\r
+ echo "You may need to run:"\r
+ echo " make -C $EDK_TOOLS_PATH/Source/C"\r
+ else\r
+ exec "$EDK_TOOLS_PATH/Source/C/bin/$cmd" "$@"\r
+ fi\r
+elif [ -e "$dir/../../Source/C/bin/$cmd" ]\r
+then\r
+ exec "$dir/../../Source/C/bin/$cmd" "$@"\r
+else\r
+ echo "Unable to find the real '$cmd' to run"\r
+ echo "This message was printed by"\r
+ echo " $0"\r
+ exit 127\r
+fi\r
+\r