20171025 src/JSON/patch/json-stream-printer.sml.patch (Datum des upstream files korrigiert)

src/JSON/patch/json-stream-printer.sml.patch

@@ -1,4 +1,4 @@
---- json-stream-printer.sml.orig	2017-10-25 01:34:17.349274000 +0200
+--- json-stream-printer.sml.orig	2017-07-14 22:32:40.000000000 +0200
 +++ json-stream-printer.sml	2017-10-25 01:43:40.211305000 +0200
 @@ -66,7 +66,7 @@
  		then TextIO.output(strm, String.extract(tenSpaces, 10-n, NONE))