# HG changeset patch # User wenzelm # Date 1548949444 -3600 # Node ID a8ee66876a1adac3e21eab9bd9f096f4ce849ad4 # Parent efb0e5332441f76b681d62bacb4b6d10a8f23a46 tuned default layout; diff -r efb0e5332441 -r a8ee66876a1a src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Thu Jan 31 16:33:57 2019 +0100 +++ b/src/Pure/Tools/main.scala Thu Jan 31 16:44:04 2019 +0100 @@ -59,7 +59,7 @@ - + """) }