# HG changeset patch
# User wenzelm
# Date 1341496989 -7200
# Node ID 07a32140ce0d44b6ccdb922ddfaa5a55ddbe1102
# Parent  c1def7433a72ae4ac0d751628ba89fc90ac0f8ea
prefer sys.exit from scala 2.9;

diff -r c1def7433a72 -r 07a32140ce0d src/Pure/System/gui_setup.scala
--- 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)
     }
   }
 }
diff -r c1def7433a72 -r 07a32140ce0d src/Pure/System/main.scala
--- a/src/Pure/System/main.scala	Thu Jul 05 15:40:57 2012 +0200
+++ b/src/Pure/System/main.scala	Thu Jul 05 16:03:09 2012 +0200
@@ -25,7 +25,7 @@
       Library.dialog(null, "Isabelle", "Isabelle output",
         Library.scrollable_text(out + "\nReturn code: " + rc))
 
-    System.exit(rc)
+    sys.exit(rc)
   }
 }