From 174dbb7e1cc703f3bc9603a18d7beadec7cd198d Mon Sep 17 00:00:00 2001 From: Tom Henderson Date: Fri, 31 Mar 2023 16:21:28 -0700 Subject: [PATCH] doc: Fix broken link on menu bar --- doc/ns3_html_theme/static/ns3_links.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/ns3_html_theme/static/ns3_links.js b/doc/ns3_html_theme/static/ns3_links.js index ef58a3755..7e5c947be 100644 --- a/doc/ns3_html_theme/static/ns3_links.js +++ b/doc/ns3_html_theme/static/ns3_links.js @@ -44,7 +44,7 @@ var ns3_man = ns3_rel + "manual/" + ns3_index; var ns3_mod = ns3_rel + "models/" + ns3_index; var ns3_tut = ns3_rel + "tutorial/" + ns3_index; var ns3_con = ns3_rel + "contributing/" + ns3_index; -var ns3_con = ns3_rel + "installation/" + ns3_index; +var ns3_ins = ns3_rel + "installation/" + ns3_index; function ns3_write_links() { document.getElementById("ns3_home1").href = ns3_home;