build: delete the install_docker script.

This gets outdated too fast. Better refer the user to docker install instructions.
scionproto · Oct 5, 2023 · 2a8b43c · 2a8b43c
1 parent dc4b786
commit 2a8b43c
Showing 1 changed file with 0 additions and 48 deletions.
diff --git a/tools/install_docker b/tools/install_docker