changeset 49558 | af7b652180d5 |
parent 49557 | 61988f9df94d |
child 49737 | dd6fc7c9504a |
--- a/src/Tools/Graphview/src/popups.scala Mon Sep 24 20:22:58 2012 +0200 +++ b/src/Tools/Graphview/src/popups.scala Mon Sep 24 21:16:33 2012 +0200 @@ -10,7 +10,7 @@ import isabelle._ import isabelle.graphview.Mutators._ import javax.swing.JPopupMenu -import scala.swing.{Action, Menu, MenuItem, Seperator} +import scala.swing.{Action, Menu, MenuItem, Separator} object Popups {