File tree Expand file tree Collapse file tree 2 files changed +7
-1
lines changed Expand file tree Collapse file tree 2 files changed +7
-1
lines changed Original file line number Diff line number Diff line change @@ -10,4 +10,10 @@ the [`docs/`](docs) directory.
10
10
11
11
For developer setup instructions, refer to [ INSTALL.md] ( INSTALL.md ) .
12
12
13
+ ## Git Workflow
14
+
15
+ PRs to this repository should target the ` develop ` branch, rather than ` master ` .
16
+ When a PR is merged to ` develop ` , a version update and release happens
17
+ automatically in CI.
18
+
13
19
[ K ] : https://github.com/runtimeverification/k
Original file line number Diff line number Diff line change @@ -9,7 +9,7 @@ version_file="package/version"
9
9
10
10
version_bump () {
11
11
local version release_commit version_major version_minor version_patch new_version current_version current_version_major current_version_minor current_version_patch
12
- version=" $1 " ; shift
12
+ version=" $( cat ${version_file} ) " ; shift
13
13
version_major=" $( echo ${version} | cut --delimiter ' .' --field 1) "
14
14
version_minor=" $( echo ${version} | cut --delimiter ' .' --field 2) "
15
15
version_patch=" $( echo ${version} | cut --delimiter ' .' --field 3) "
You can’t perform that action at this time.
0 commit comments