src/Pure/System/gui_setup.scala
changeset 48710 5b51ccdc8623
parent 48192 07a32140ce0d
child 50652 ead5714cc480
equal deleted inserted replaced
48709:719f458cd89e 48710:5b51ccdc8623