Index: platform_tools/ios/bin/ios_pull_if_needed |
diff --git a/platform_tools/ios/bin/ios_pull_if_needed b/platform_tools/ios/bin/ios_pull_if_needed |
new file mode 100755 |
index 0000000000000000000000000000000000000000..e07bc32878d4b68fd8c649f1db18d56a4c027d9e |
--- /dev/null |
+++ b/platform_tools/ios/bin/ios_pull_if_needed |
@@ -0,0 +1,12 @@ |
+#!/bin/bash |
+ |
+# Fail-fast if anything in the script fails. |
+set -e |
+ |
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" |
+source $SCRIPT_DIR/ios_setup.sh |
+ |
+HOST_PATH=$1 |
+DEVICE_PATH=$2 |
+ |
+ios_pull $HOST_PATH $DEVICE_PATH |