diff options
Diffstat (limited to 'bin/reproducible_common.sh')
| -rwxr-xr-x | bin/reproducible_common.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/bin/reproducible_common.sh b/bin/reproducible_common.sh index 8b382c23..9a6b8656 100755 --- a/bin/reproducible_common.sh +++ b/bin/reproducible_common.sh @@ -367,6 +367,7 @@ write_page_intro() { fi } +# See the python equivelent of this function: reproducible_common.py's create_default_page_footer write_page_footer() { write_page "<hr id=\"footer_separator\" /><p style=\"font-size:0.9em;\"><div id=\"page_footer\">" if [ -n "$JOB_URL" ] ; then |