# HG changeset patch
# User blanchet
# Date 1472567987 -7200
# Node ID 4e078ae3682cb1717b1c52711af33fb1cf067483
# Parent  2d21591967bc1733660bcff9482fa3e37863a1d4
tuned final stop in message

diff -r 2d21591967bc -r 4e078ae3682c src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Tue Aug 30 09:04:40 2016 +0200
+++ b/src/Tools/solve_direct.ML	Tue Aug 30 16:39:47 2016 +0200
@@ -79,11 +79,11 @@
           let val msg = Pretty.string_of (Pretty.chunks (message results))
           in if mode = Auto_Try then [msg] else (writeln msg; []) end)
     | SOME NONE =>
-        (if mode = Normal then writeln "No proof found."
+        (if mode = Normal then writeln "No proof found"
          else ();
          (noneN, []))
     | NONE =>
-        (if mode = Normal then writeln "An error occurred."
+        (if mode = Normal then writeln "An error occurred"
          else ();
          (unknownN, [])))
   end