diff options
| author | Remi Collet <fedora@famillecollet.com> | 2015-07-14 08:52:32 +0200 |
|---|---|---|
| committer | Remi Collet <fedora@famillecollet.com> | 2015-07-14 08:52:32 +0200 |
| commit | 281d00402c1d83cc0c403515b7d7a02921236aa1 (patch) | |
| tree | 444b3439846d9b7d4d03dcef3ef9f03afdee6814 /php-JMSParser-strip.sh | |
| parent | ffec025b1b448e93b69ab2ca1ff74a95301e6c1b (diff) | |
php-JMSParser: backport fedora changes
Diffstat (limited to 'php-JMSParser-strip.sh')
| -rwxr-xr-x | php-JMSParser-strip.sh | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/php-JMSParser-strip.sh b/php-JMSParser-strip.sh deleted file mode 100755 index b155801..0000000 --- a/php-JMSParser-strip.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash - -if [ $# != 2 ]; then - echo "Usage: $0 VERSION GITHUB_COMMIT" 1>&2 - exit 1 -fi - -VERSION=$1 -GITHUB_COMMIT=$2 - -ORIGINAL_SOURCE_FILE="${GITHUB_COMMIT}.tar.gz" -NEW_SOURCE_FILE="php-JMSParser-${VERSION}-${GITHUB_COMMIT}.tar.gz" - -if [ ! -f "$ORIGINAL_SOURCE_FILE" ]; then - echo "ERROR: Original source file '${ORIGINAL_SOURCE_FILE}' not found" 1>&2 - exit 1 -fi - -TAR=`which tar` - -$TAR -xzf "$ORIGINAL_SOURCE_FILE" -rm -rf "parser-lib-${GITHUB_COMMIT}/doc" "$NEW_SOURCE_FILE" -$TAR -czf "$NEW_SOURCE_FILE" "parser-lib-${GITHUB_COMMIT}" - -echo "${NEW_SOURCE_FILE} created" -exit 0 |