diff options
| author | Jason Gross | 2014-09-09 14:32:11 -0400 |
|---|---|---|
| committer | Jason Gross | 2014-09-09 14:33:19 -0400 |
| commit | ad1a964c7c1a03287c501ec4de1242640ddc9265 (patch) | |
| tree | a51376d313b89bbcc6e4dbb902f879ff128821df | |
| parent | 0978120752ce0546de113b890bdd974413352685 (diff) | |
Support environments where `find` is Windows' find
| -rwxr-xr-x | dev/make-sdk-win32.sh | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/dev/make-sdk-win32.sh b/dev/make-sdk-win32.sh index 2c3713b5dc..27c7f6a961 100755 --- a/dev/make-sdk-win32.sh +++ b/dev/make-sdk-win32.sh @@ -38,6 +38,16 @@ has_spaces() { REVISION=1 BASE="/cygdrive/c/CoqSDK-$REVISION" +# Windows has a version of FIND in C:/Windows/system32/find, and we don't want to use that +if [ -x /usr/bin/find ] +then + FIND=/usr/bin/find +else + echo "WARNING: /usr/bin/find does not exist. Falling back on:" + which find + FIND=find +fi + WGET_ARGS="-N -q" if [ "$(has_spaces $BASE; echo $?)" -ne 0 ]; then @@ -149,7 +159,7 @@ install_ocaml() { cp -r tmp/\$_OUTDIR/lib "$BASE/" cp -r tmp/lib "$BASE/" cp -r tmp/\$_OUTDIR/etc "$BASE/" - find "$BASE" -name '*.dll' -o -name '*.exe' | tr '\n' '\0' \ + "$FIND" "$BASE" -name '*.dll' -o -name '*.exe' | tr '\n' '\0' \ | xargs -0 chmod a+x mv "$BASE/lib/topfind" "$BASE/lib/topfind.in" sed -i 's|@SITELIB@|@BASE@/lib/site-lib|g' "$BASE/lib/topfind.in" |