src/Pure/System/gui_setup.scala
changeset 48192 07a32140ce0d
parent 48017 9f7b27635b57
child 50652 ead5714cc480
--- a/src/Pure/System/gui_setup.scala	Thu Jul 05 15:40:57 2012 +0200
+++ b/src/Pure/System/gui_setup.scala	Thu Jul 05 16:03:09 2012 +0200
@@ -62,7 +62,7 @@
     // reactions
     listenTo(ok)
     reactions += {
-      case ButtonClicked(`ok`) => System.exit(0)
+      case ButtonClicked(`ok`) => sys.exit(0)
     }
   }
 }