Reading/Web/Release process/How to release

From mediawiki.org

A release can be made by the following commands

First generate the release settings the commit message with the `Release` prefix.

 git merge --no-ff origin/dev

Update the release number in extension.json Find the commit sha of the last release and run the following script

git log <commit>.. --pretty=format:'%h %s' --reverse | grep -v '^.\{7\} Merge\|Localisation\|Release' | cat - HISTORY > HISTORY.tmp && mv HISTORY.tmp HISTORY
echo '==QuickSurveys <version>=='| cat - HISTORY > HISTORY.tmp && mv HISTORY.tmp HISTORY

Amend the commit with the changes and then submit it using git review master.

Note: If you are doing a first release you can determine the very first commit using:

git rev-list --max-parents=0 HEAD

and you will need to setup a HISTORY file

touch HISTORY