src/Tools/jEdit/jedit_main/build.props
changeset 73994 fbb30dac95a2
parent 73987 fc363a3b690a
child 74029 0701ff55780d
equal deleted inserted replaced
73993:3868fed3c34b 73994:fbb30dac95a2
     9   dockables.xml \
     9   dockables.xml \
    10   plugin.props \
    10   plugin.props \
    11   services.xml
    11   services.xml
    12 sources = \
    12 sources = \
    13   isabelle_sidekick.scala \
    13   isabelle_sidekick.scala \
       
    14   dockables.scala \
    14   plugin.scala \
    15   plugin.scala \
    15   scala_console.scala
    16   scala_console.scala \
       
    17   services.scala