Add a link to the static index of generated WWW pages
Change-Id: Ic1528bd9d386660090fe4fae4908bf663f314db2
This commit is contained in:
parent
43518efb88
commit
5979d8093d
|
@ -1167,6 +1167,10 @@ def generate_index_file():
|
|||
(path, f, f))
|
||||
index_file.write('<br/>\n')
|
||||
|
||||
if os.path.is_file(os.path.join(get_publish_path(), 'www-index.html')):
|
||||
index_file.write('<br/>\n')
|
||||
index_file.write('<a href="www-index.html">list of generated '
|
||||
'WWW pages</a>\n')
|
||||
index_file.write('</body>\n'
|
||||
'</html>\n')
|
||||
index_file.close()
|
||||
|
|
Loading…
Reference in New Issue