diff options
| author | Chris Lamb <lamby@debian.org> | 2015-09-10 22:25:31 +0100 |
|---|---|---|
| committer | Holger Levsen <holger@layer-acht.org> | 2015-09-11 10:35:54 +0200 |
| commit | 3a36114f1f70fe80cec43b568eabd15e166f1c25 (patch) | |
| tree | def4b3f220bf10f6b5e63b2138ebc84718452244 | |
| parent | eca5f99b6f2f8f8b571e8753d11b46894b534e1d (diff) | |
| download | jenkins.debian.net-3a36114f1f70fe80cec43b568eabd15e166f1c25.tar.xz | |
Support meta-refresh header
Signed-off-by: Chris Lamb <lamby@debian.org>
| -rwxr-xr-x | bin/reproducible_common.py | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/bin/reproducible_common.py b/bin/reproducible_common.py index df8374cd..38163ca0 100755 --- a/bin/reproducible_common.py +++ b/bin/reproducible_common.py @@ -122,6 +122,7 @@ html_header = Template("""<!DOCTYPE html> <head> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="viewport" content="width=device-width" /> + $meta_refresh <link href="/static/style.css" type="text/css" rel="stylesheet" /> <title>$page_title</title> </head> @@ -281,14 +282,17 @@ def _gen_links(suite, arch): return html -def write_html_page(title, body, destfile, suite=defaultsuite, arch=defaultarch, noheader=False, style_note=False, noendpage=False, packages=False): +def write_html_page(title, body, destfile, suite=defaultsuite, arch=defaultarch, noheader=False, style_note=False, noendpage=False, packages=False, refresh_every=None): now = datetime.utcnow().strftime('%Y-%m-%d %H:%M UTC') html = '' # this removes the padding if we are writing a package page padding = 'class="wrapper"' if packages else '' + meta_refresh = '<meta http-equiv="refresh" content="%d">' % \ + refresh_every if refresh_every is not None else '' html += html_header.substitute( page_title=title, - padding=padding) + padding=padding, + meta_refresh=meta_refresh) if not noheader: links = _gen_links(suite, arch) html += html_head_page.substitute( |