# HG changeset patch
# User wenzelm
# Date 1586026416 -7200
# Node ID b3f738f12a9a3b0146eba7b2865f3e3231953521
# Parent  220d19f3e0741ed4be5c620537c11095edd55647
tuned names;

diff -r 220d19f3e074 -r b3f738f12a9a src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Sat Apr 04 20:16:25 2020 +0200
+++ b/src/Pure/General/file_watcher.scala	Sat Apr 04 20:53:36 2020 +0200
@@ -90,7 +90,7 @@
       handle(changed)
     }
 
-    private val watcher_thread = Standard_Thread.fork(name = "File_Watcher", daemon = true)
+    private val watcher_thread = Standard_Thread.fork(name = "file_watcher", daemon = true)
     {
       try {
         while (true) {
diff -r 220d19f3e074 -r b3f738f12a9a src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Sat Apr 04 20:16:25 2020 +0200
+++ b/src/Pure/System/command_line.scala	Sat Apr 04 20:53:36 2020 +0200
@@ -26,7 +26,7 @@
   def tool(body: => Unit)
   {
     val thread =
-      Standard_Thread.fork(name = "isabelle", inherit_locals = true) {
+      Standard_Thread.fork(name = "command_line", inherit_locals = true) {
         val rc =
           try { body; 0 }
           catch {