IMPORTANT NOTES (please read, then delete):
-
The PR title should start with "Fix #bugnum: " (if applicable), followed by a clear one-line present-tense summary of the changes introduced in the PR. For example: "Fix #bugnum: introduce the first version of the collection editor.".
-
Please make sure to mention "#bugnum" somewhere in the description of the PR. This enables Github to link the PR to the corresponding bug.
Please also make sure to follow the style rules.