From 707918da815fab1b927195daa63fdd0394755ef3 Mon Sep 17 00:00:00 2001 From: Max Horn Date: Sun, 7 May 2017 18:43:31 +0200 Subject: [PATCH] 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. --- etc/install-tools.sh | 27 --------------------------- 1 file changed, 27 deletions(-) delete mode 100755 etc/install-tools.sh diff --git a/etc/install-tools.sh b/etc/install-tools.sh deleted file mode 100755 index c7bb60ce95..0000000000 --- a/etc/install-tools.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/bin/sh -############################################################################# -## -## -## This script unpacks the tools.tar.gz archive which contains some utilities -## mainly for package authors (preparing documentation and archives, ...). -## -## The content of the archive will go to the 'doc' and 'dev' subdirectories -## of the GAP root directory. To ensure that they will go to the correct -## destination, run this script *ONLY* from the 'etc' directory where it is -## located (same directory with the tools.tar.gz archive). - -if [ -f tools.tar.gz ] -then -echo '============================================================================' -echo 'Unpacking tools.tar.gz archive ...' -tar -xvzf tools.tar.gz -C ../ -echo 'Done!' -echo '============================================================================' -else -echo '============================================================================' -echo 'Error in install-tools.sh: can not find tools.tar.gz archive!' -echo 'Please run install-tools.sh from the dev directory of your GAP installation!' -echo '============================================================================' -fi - -