stop-all-dockers 854 B

1234567891011121314151617181920212223242526272829303132333435363738394041
  1. #!/bin/bash
  2. # Stop all five sets of dockers. This is useful if, for example, a run
  3. # of repro-all-dockers is interrupted, leaving some dockers (and
  4. # potentionally the processes therein) running.
  5. # cd into the directory containing this script (from the bash faq 028)
  6. if [[ $BASH_SOURCE = */* ]]; then
  7. cd -- "${BASH_SOURCE%/*}/" || exit
  8. fi
  9. # PRAC
  10. echo Stopping PRAC dockers
  11. echo
  12. ( cd ../docker && ./stop-docker ) || exit 1
  13. # Duoram
  14. echo
  15. echo Stopping Duoram dockers
  16. echo
  17. ( cd comps/duoram/Docker && ./stop-docker ) || exit 1
  18. # Floram
  19. echo
  20. echo Stopping Floram dockers
  21. echo
  22. ( cd comps/floram && ./stop-docker ) || exit 1
  23. # Circuit ORAM
  24. echo
  25. echo Stopping Circuit ORAM dockers
  26. echo
  27. ( cd comps/circuit-oram/docker && ./stop-docker ) || exit 1
  28. # Ramen
  29. echo
  30. echo Stopping Ramen dockers
  31. echo
  32. ( cd comps/ramen/Docker && ./stop-docker ) || exit 1
  33. echo