diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-06-24 13:53:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-06-24 13:53:19 +0000 |
| commit | a9c08e799500d19e9dcc9d9eb46a70f8478b8499 (patch) | |
| tree | f38ea851a557bcde1d4352928c7cdf965df85854 /images/Makefile | |
| parent | 56bef7d39ad63ca18ec706613a0e99b524d5f367 (diff) | |
Updates and new images
Diffstat (limited to 'images/Makefile')
| -rw-r--r-- | images/Makefile | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/images/Makefile b/images/Makefile index 62e5943a..a5f35f56 100644 --- a/images/Makefile +++ b/images/Makefile @@ -20,11 +20,14 @@ # Sources BUTTONS=goal.xcf next.xcf qed.xcf restart.xcf retract.xcf undo.xcf use.xcf -WEBPIX=isabelle_transparent.xcf ProofGeneral.xcf text_general.xcf text_proof.xcf +WEBPIX=isabelle_transparent.xcf ProofGeneral.xcf pg-text.xcf # Targets for html directory WEBPIX_ONLY= -WEBPIX_TARGETS=$(WEBPIX_ONLY) ProofGeneral.jpg text_general.gif text_proof.gif +WEBPIX_TARGETS=$(WEBPIX_ONLY) ProofGeneral.jpg pg-text.gif +# Targets for doc directory +DOCPIX_TARGETS=ProofGeneral.jpg + # Junk not wanted UNWANTED=text_general.jpg text_proof.jpg @@ -66,7 +69,9 @@ clean: rm -f $(WEBPIX_ONLY) $(UNWANTED) install: webpix - cp -pf $(WEBPIX_TARGETS) ../html + cp -pf $(WEBPIX_TARGETS) ../html/images + cp -pf $(DOCPIX_TARGETS) ../doc + ## ## Batch mode is a bit broken on The Gimp at the moment (v 1.0) ## For script fu, at least, it seems tricky to pass arguments to |