Skip to content

Instantly share code, notes, and snippets.

@davidedelpapa
Created July 25, 2020 13:09
Show Gist options
  • Save davidedelpapa/8e1aa4145b4841853cd67dde31115678 to your computer and use it in GitHub Desktop.
Save davidedelpapa/8e1aa4145b4841853cd67dde31115678 to your computer and use it in GitHub Desktop.
#!/bin/sh
stop(){
if [ -f .serverpid ]; then
kill $(cat .serverpid)
rm .serverpid
echo Server stopped
else
echo Could not find the server PID. Is it running?
fi
}
stop
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment