From 5c0ebdcb647aa3fba2407fef63f9734db5322ae3 Mon Sep 17 00:00:00 2001 From: Fred Drake Date: Fri, 5 Nov 2004 04:05:06 +0000 Subject: [PATCH] - make the default image type PNG, to match mkhowto - add a command-line option to control the image type --- Doc/tools/support.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Doc/tools/support.py b/Doc/tools/support.py index cd42fd0060d..fc4cafaf878 100644 --- a/Doc/tools/support.py +++ b/Doc/tools/support.py @@ -20,7 +20,9 @@ class Options: # content components "address=", "iconserver=", "favicon=", - "title=", "uplink=", "uptitle="] + "title=", "uplink=", "uptitle=", + "image-type=", + ] outputfile = "-" columns = 1 @@ -51,7 +53,7 @@ class Options: self.args = [] self.variables = {"address": "", "iconserver": "icons", - "imgtype": "gif", + "imgtype": "png", "title": "Global Module Index", } @@ -93,6 +95,8 @@ class Options: self.variables["iconserver"] = val.strip() or "." elif opt == "--favicon": self.favicon = val.strip() + elif opt == "--image-type": + self.variables["imgtype"] = val.strip() else: self.handle_option(opt, val) if self.uplink and self.uptitle: