diff --git a/docs/build_docs/update_html.py b/docs/build_docs/update_html.py index 3822119d..dc8683f9 100644 --- a/docs/build_docs/update_html.py +++ b/docs/build_docs/update_html.py @@ -28,19 +28,38 @@ def update_version_link(version, folder_name, index_file): {}▼

Click link above to switch version

'''.format(index_path, folder_name) - #print(index_buf.find(key_str)) index_buf = index_buf.replace(key_str, version_list) - #print(index_buf) with open(index_file, "w") as f: f.write(index_buf) +def update_search(folder): + search_file_name="{}/search.html".format(folder) + + with open(search_file_name, "r") as f: + index_buf = f.read() + key_str='' + version_list = ''' + + + + + + + ''' + index_buf = index_buf.replace(key_str, version_list) + + with open(search_file_name, "w") as f: + f.write(index_buf) + def main(folder, version): folder_name=os.path.basename(folder) for index_file in glob.glob('{}/**/*.html'.format(folder),recursive = True): update_version_link(version, folder_name, index_file) - + update_search(folder) def help(me): print("python {} html_folder version".format(me))