src/Tools/GraphBrowser/etc/build.props
author wenzelm
Fri, 16 Jul 2021 12:40:39 +0200
changeset 74013 f114e11fe21d
parent 74011 1d366486a812
child 74015 12b1f4649ab1
permissions -rw-r--r--
clarified directory;

description = graph browser
lib = $ISABELLE_HOME/lib/classes
name = GraphBrowser
javac_options = -source 7 -target 7
sources = \
  GraphBrowser/AWTFontMetrics.java \
  GraphBrowser/AbstractFontMetrics.java \
  GraphBrowser/Box.java \
  GraphBrowser/Console.java \
  GraphBrowser/DefaultFontMetrics.java \
  GraphBrowser/Directory.java \
  GraphBrowser/DummyVertex.java \
  GraphBrowser/Graph.java \
  GraphBrowser/GraphBrowser.java \
  GraphBrowser/GraphBrowserFrame.java \
  GraphBrowser/GraphView.java \
  GraphBrowser/NormalVertex.java \
  GraphBrowser/ParseError.java \
  GraphBrowser/Region.java \
  GraphBrowser/Spline.java \
  GraphBrowser/TreeBrowser.java \
  GraphBrowser/TreeNode.java \
  GraphBrowser/Vertex.java \
  awtUtilities/Border.java \
  awtUtilities/MessageDialog.java \
  awtUtilities/TextFrame.java