rustdoc: add comment about numeric spacing

Author: notriddle

src/librustdoc/html/static/js/search.js

@@ -2335,6 +2335,10 @@ ${item.displayPath}<span class="${type}">${name}</span>\
 
     function makeTabHeader(tabNb, text, nbElems) {
         // https://blog.horizon-eda.org/misc/2020/02/19/ui.html
+        //
+        // CSS runs with `font-variant-numeric: tabular-nums` to ensure all
+        // digits are the same width. \u{2007} is a Unicode space character
+        // that is defined to be the same width as a digit.
         const fmtNbElems =
             nbElems < 10  ? `\u{2007}(${nbElems})\u{2007}\u{2007}` :
             nbElems < 100 ? `\u{2007}(${nbElems})\u{2007}` :