include Sidekick its dependency ErrorList in dist
authorimmler@in.tum.de
Tue, 02 Dec 2008 15:25:24 +0100
changeset 34395 287f3ecdfc2a
parent 34394 7878d1100510
child 34396 de809360c51d
include Sidekick its dependency ErrorList in dist
src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Sun Nov 30 19:32:17 2008 +0100
+++ b/src/Tools/jEdit/makedist	Tue Dec 02 15:25:24 2008 +0100
@@ -93,6 +93,8 @@
 cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
 cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
 cp jars/lib/core-renderer.jar "$JEDIT/jars/"
+cp jars/lib/ErrorList.jar "$JEDIT/jars/"
+cp jars/lib/SideKick.jar "$JEDIT/jars/"
 
 
 # build archive