src/Pure/Tools/build.scala
changeset 71960 6a64205b491a
parent 71896 ce06d6456cc8
child 71968 ec0ef3ebe75e
equal deleted inserted replaced
71958:4320875eb8a1 71960:6a64205b491a
   490     val build_options =
   490     val build_options =
   491       options +
   491       options +
   492         "ML_statistics" +
   492         "ML_statistics" +
   493         "completion_limit=0" +
   493         "completion_limit=0" +
   494         "editor_tracing_messages=0" +
   494         "editor_tracing_messages=0" +
       
   495         "pide_exports=false" +
   495         "pide_reports=false"
   496         "pide_reports=false"
   496 
   497 
   497     val store = Sessions.store(build_options)
   498     val store = Sessions.store(build_options)
   498 
   499 
   499     Isabelle_Fonts.init()
   500     Isabelle_Fonts.init()