Skip to content

Instantly share code, notes, and snippets.

@floreo
Created May 2, 2017 19:24
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save floreo/5a3fecacd97f7056973a67d59fd01827 to your computer and use it in GitHub Desktop.
Save floreo/5a3fecacd97f7056973a67d59fd01827 to your computer and use it in GitHub Desktop.
Simple pid script
#!/usr/bin/env bash
_pid="$HOME/$0.pid"
while :
do
if [ ! -s "${_pid}" ] ; then
echo $$ >"${_pid}"
echo "Doing real stuff"
rm "${_pid}"
break
else
echo "waiting for $(cat ${_pid}) to finish"
sleep 10
fi
done
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment