src/Pure/System/scala.scala
changeset 72760 042180540068
parent 72756 72ac27ea12b2
child 72763 3cc73d00553c
equal deleted inserted replaced
72759:bd5ee3148132 72760:042180540068
   240 
   240 
   241 class Scala_Functions extends Scala.Functions(
   241 class Scala_Functions extends Scala.Functions(
   242   Scala.Echo,
   242   Scala.Echo,
   243   Scala.Sleep,
   243   Scala.Sleep,
   244   Scala.Toplevel,
   244   Scala.Toplevel,
       
   245   Doc.Doc_Names,
   245   Bibtex.Check_Database)
   246   Bibtex.Check_Database)