Merge branch 'better-json-fix' into json-fix-extended
authorChristian Femers <femers@in.tum.de>
Tue, 3 Sep 2019 05:47:55 +0000 (07:47 +0200)
committerChristian Femers <femers@in.tum.de>
Tue, 3 Sep 2019 05:47:55 +0000 (07:47 +0200)
commitccf83da0021c673571ef8d8e42631d76808d6b3d
tree6eda616fc67ce2047199708d1f0eef87ed168980
parentaacd9de307f43bd19065ace45688a49af064f5a5
parent3ac35259a780dcc3c6a2bfab5251121874cd5d80
Merge branch 'better-json-fix' into json-fix-extended