etc/install-tools.sh: remove

All this script does is to extract a tar file. Anybody who really needs to do that can just do it directly, without need for a script.
gap-system · May 31, 2017 · 1204222 · 1204222
1 parent 1745ccd
commit 1204222
Showing 1 changed file with 0 additions and 27 deletions.
diff --git a/etc/install-tools.sh b/etc/install-tools.sh