# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737476152 -3600
# Node ID f1d520cd7575cc29af16f585312beee6a3321fad
# Parent  560c7ff87f748b5cd7bb8b0c499b7c8850f21df0
clarified find_facts URL;

diff -r 560c7ff87f74 -r f1d520cd7575 NEWS
--- a/NEWS	Tue Jan 21 17:13:06 2025 +0100
+++ b/NEWS	Tue Jan 21 17:15:52 2025 +0100
@@ -361,7 +361,7 @@
 
     isabelle find_facts_index HOL
     isabelle find_facts_server
-    open http://localhost:8080/app#search?q=Hilbert
+    open http://localhost:8080/find_facts#search?q=Hilbert
 
 Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
 
diff -r 560c7ff87f74 -r f1d520cd7575 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 17:13:06 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 17:15:52 2025 +0100
@@ -924,7 +924,7 @@
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
           },
-          new HTTP.Service("app") {
+          new HTTP.Service("find_facts") {
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               Some(HTTP.Response.html(
                 if (devel) project.build_html(progress = progress) else frontend))
@@ -951,7 +951,7 @@
           }))
 
       server.start()
-      progress.echo("Server started " + server.toString + "/app")
+      progress.echo("Server started " + server.toString + "/find_facts")
 
       @tailrec
       def loop(): Unit = {