--- old+++ new@@ -2,3 +2,7 @@* Add an operator+(State, double) and the corresponding operator-
* Replace code where this is currently worked around
++----++Did not find a good position where this is used, but the implementation was cheap enough, so I did it nevertheless.
status: assigned --> done
assigned_to: Ulf Lorenz --> nobody
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Diff: