isabelle: lib/browser/Makefile@a6d0428dea8e (annotated)

3598 28b6670e415a Makefile for GraphBrowser berghofe parents: diff changeset	1	# $Id$
28b6670e415a Makefile for GraphBrowser berghofe parents: diff changeset	2
14539 90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	3	DST=classes
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	4
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	5	all: GraphBrowser.jar
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	6
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	7	GraphBrowser.jar: GraphBrowser/.java awtUtilities/.java
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	8	mkdir -p $(DST)
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	9	javac -d $(DST) GraphBrowser/GraphBrowser.java GraphBrowser/Console.java
14545 71b9ef3d047f change order of options for jar (fix error on Sun) kleing parents: 14539 diff changeset	10	jar cf GraphBrowser.jar -C $(DST) .
14539 90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	11	rm -rf $(DST)
13971 aa5b6c8c7c4c target clean, compile Console.java kleing parents: 11980 diff changeset	12
aa5b6c8c7c4c target clean, compile Console.java kleing parents: 11980 diff changeset	13	clean:
aa5b6c8c7c4c target clean, compile Console.java kleing parents: 11980 diff changeset	14	rm -f GraphBrowser/*.class
aa5b6c8c7c4c target clean, compile Console.java kleing parents: 11980 diff changeset	15	rm -f awtUtilities/*.class
14539 90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	16	rm -rf $(DST)
90c625edaee1 produce jar instead of single .class files kleing parents: 13971 diff changeset	17	rm -f GraphBrowser.jar

author	urbanc
	Thu, 13 Sep 2007 23:58:38 +0200
changeset 24571	a6d0428dea8e
parent 14545	71b9ef3d047f
child 25437	1170e384764d
permissions	-rw-r--r--