14 Aug
2014
14 Aug
'14
6:21 p.m.
On Thu, Aug 14, 2014 at 1:38 PM, Johannes Sch önberger <jsch@demuc.de> wrote:
Just a reminder: before merging a PR in the future, we want to make sure, that the changes are documented in `doc/release/release_dev.txt`.
Ouch, good point--thanks for the reminder. Stéfan