Correct comment

Author: tristanlatr

pydoctor/themes/base/search.js

@@ -465,9 +465,9 @@ window.addEventListener("click", (event) => {
   }
 });
 
-// Focus on the search bar when the user hit '/' or 'ctrl+k' key, this replaces the default readthedocs search
-// box which is not going to include any of the API documentation in its index at the moment. See
-// issue #356 for more details.
+// Focus on the search bar when the user hit '/' or 'ctrl+k' key, the '/' shortcut is replaced by the default readthedocs search
+// box which is not going to include any of the API documentation in its index at the moment (see
+// issue #356), this is why we provide another shortcut which is commonly associated to searching.
 window.addEventListener('keydown', (event) => {
   if((event.key === 'k' && (event.ctrlKey || event.metaKey)) || (event.key === '/' && !event.ctrlKey && !event.metaKey && !event.altKey)){
     event.preventDefault();