diff options
-rwxr-xr-x | debian/purify_tarball | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/purify_tarball b/debian/purify_tarball index 52d54ac7..a453db06 100755 --- a/debian/purify_tarball +++ b/debian/purify_tarball @@ -6,7 +6,7 @@ CURDIR=`pwd` ORIG=$1 WORKDIR=`dirname $ORIG` ORIGFILE=`basename $ORIG` -VERSION=`echo "$ORIGFILE" | sed "s/^coq-\([0-9\.a-z]\+\)\.tar\.gz$/\1/"` +VERSION=`echo "$ORIGFILE" | sed "s/^coq-\([0-9\.a-z-]\+\)\.tar\.gz$/\1/"` cd $WORKDIR |