diff --git a/src/Misc/layoutroot/safe_sleep.sh b/src/Misc/layoutroot/safe_sleep.sh index 7ba5be325e8..94254ee104e 100644 --- a/src/Misc/layoutroot/safe_sleep.sh +++ b/src/Misc/layoutroot/safe_sleep.sh @@ -1,6 +1,15 @@ #!/bin/bash SECONDS=0 -while [[ $SECONDS != $1 ]]; do + +# Bash 4.0 and above supports read. +if [[ -n "$BASH_VERSINFO" && "${BASH_VERSINFO[0]}" -ge 4 ]]; then + echo foo + # Bash has no sleep builtin, but read with a timeout can behave in same way. + read -rt "$1" <> <(:) || : +fi +# Fallback to busy wait. +while [[ $SECONDS -lt $1 ]]; do + echo bar : done