# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739289773 -3600
# Node ID 39f2662c8fb02fc8be7f3be7246ba02b288138a2
# Parent  fb684af6b397e4d5b96df008cec4ac942c356b37
handle path change properly;

diff -r fb684af6b397 -r 39f2662c8fb0 src/Tools/Find_Facts/web/src/Main.elm
--- a/src/Tools/Find_Facts/web/src/Main.elm	Tue Feb 11 17:01:28 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Main.elm	Tue Feb 11 17:02:53 2025 +0100
@@ -82,6 +82,7 @@
 
 
 {- url encoding/decoding -}
+{- NB: routing only in URL fragment. -}
 
 aboutN = "about"
 searchN = "search"
@@ -164,7 +165,9 @@
   case msg of
     Link_Clicked urlRequest ->
       case urlRequest of
-        Browser.Internal url -> (model, push_url True model.nav_key url)
+        Browser.Internal url ->
+          if url.path == model.url.path then (model, push_url True model.nav_key url)
+          else (model, Navigation.load (Url.toString url))
         Browser.External href -> (model, Navigation.load href)
 
     Url_Changed url ->