projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
4643949
)
minor fix to release script
author
Morgan Deters
<mdeters@gmail.com>
Fri, 30 Nov 2012 14:07:11 +0000
(14:07 +0000)
committer
Morgan Deters
<mdeters@gmail.com>
Fri, 30 Nov 2012 14:07:11 +0000
(14:07 +0000)
contrib/cut-release
patch
|
blob
|
history
diff --git
a/contrib/cut-release
b/contrib/cut-release
index 0870b6ce06764df66fd71f6ed5ef7a35e7d52ebe..ea0308adab4e6035ab99649caf5eada5d1eb17f2 100755
(executable)
--- a/
contrib/cut-release
+++ b/
contrib/cut-release
@@
-91,7
+91,7
@@
if [ -z "$root" ]; then
fi
echo "Checking repo for unmerged updates..."
-if [ `svn -uq status | wc -l` -ne 1 ]; then
+if [ `svn -uq status |
grep -v '^M *[0-9]* *NEWS$' |
wc -l` -ne 1 ]; then
echo "$(basename "$0"): ERROR: This working directory isn't up to date" 2>&1
$dryrun || exit 1
fi