diff options
Diffstat (limited to 'bin')
| -rwxr-xr-x | bin/reproducible_common.sh | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/bin/reproducible_common.sh b/bin/reproducible_common.sh index 395db22e..fd409100 100755 --- a/bin/reproducible_common.sh +++ b/bin/reproducible_common.sh @@ -163,6 +163,11 @@ write_page_header() { done write_page "<li><a href=\"$BASEURL/index_${TARGET}.html\">${SPOKEN_TARGET}</a></li>" done + for i in $SUITES ; do + if [ "$i" != "$SUITE" ] ; then + write_page "<li><a href=\"$i\">suite: $i</a></li>" + fi + done write_page "</ul>" write_page "</header>" } |