
Aug. 14, 2014
4:38 a.m.
Hi everyone, 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`. Johannes Schönberger