Skip to content

Commit 75c3c8a

Browse files
committed
Improve dist script.
1 parent 26abb55 commit 75c3c8a

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

dist.sh

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,16 @@ git checkout -b release-$VERSION
2626
oasis setup
2727

2828
# Remove this script and dev-files
29-
rm -f dist.sh opam .jenkins.sh
29+
rm -f dist.sh .jenkins.sh
30+
31+
# Fix the version in the opam files.
32+
sed -i -e "s/version: \"dev\"/version: \"${VERSION}\"/" *.opam
3033

3134
# Commit
3235
git add --all --force
3336
git commit
3437
git tag $VERSION
3538

3639
git checkout master
40+
41+
# Prepare publishing

0 commit comments

Comments
 (0)