Going to merge this, but undecided when. Before we merge the pull request, I need to finish the logging in the Introducelogging branch and merge that to master. Then, it's probably a good moment to merge. It's good you only need very trivial changes to the server, that makes it easy. Thx!
Going to merge this, but undecided when. Before we merge the pull request, I need to finish the logging in the Introducelogging branch and merge that to master. Then, it's probably a good moment to merge. It's good you only need very trivial changes to the server, that makes it easy. Thx!