From d4349c8b0ab5fefdc87f4764c1a788d3b00824bf Mon Sep 17 00:00:00 2001
From: Marek Kaluba <kalmar@amu.edu.pl>
Date: Wed, 23 Feb 2022 16:28:46 +0100
Subject: [PATCH] add label to search field

---
 docs/morphisms/js/morphisms.js | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/docs/morphisms/js/morphisms.js b/docs/morphisms/js/morphisms.js
index 27e7e7b..abb07ad 100644
--- a/docs/morphisms/js/morphisms.js
+++ b/docs/morphisms/js/morphisms.js
@@ -39,6 +39,10 @@ async function add_search() {
         .attr("id", "datalistOptions")
         ;
 
+    input_grp.insert("div")
+        .classed("form-text", true)
+        .text("Or click to highlight descendants")
+        ;
 }
 
 async function switch_katex(toggle=true) {