From 36af779dee0e1003cc8b6e37e8e7940e8465b212 Mon Sep 17 00:00:00 2001 From: jacob-buehler <86370501+jacob-buehler@users.noreply.github.com> Date: Thu, 3 Aug 2023 18:03:14 -0400 Subject: [PATCH] Fix hyperlink to profiler options (#1003) * update * EOF line --- docs/update_documentation.py | 10 ++++++++++ profiler_options.html | 1 + 2 files changed, 11 insertions(+) create mode 100644 profiler_options.html diff --git a/docs/update_documentation.py b/docs/update_documentation.py index e780243bc..93d5d8b19 100644 --- a/docs/update_documentation.py +++ b/docs/update_documentation.py @@ -74,3 +74,13 @@ ) index_file.write(redirect_link) index_file.close() + +# update the profiler_options.html file to redirect to detailed options docs +index_file = open("../profiler_options.html", "w") +redirect_link = ( + '' +) +index_file.write(redirect_link) +index_file.close() diff --git a/profiler_options.html b/profiler_options.html new file mode 100644 index 000000000..e8407a9ff --- /dev/null +++ b/profiler_options.html @@ -0,0 +1 @@ +