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 7, 2017 · 5bdcb50 · 5bdcb50
1 parent 694bd74
commit 5bdcb50
Showing 1 changed file with 0 additions and 27 deletions.
diff --git a/etc/install-tools.sh b/etc/install-tools.sh