fix: jump to search for operand

Jacky Zhao

2022-11-22 e374e3abd42c1719ad1fdc6bd9c641efb2ddf954

 assets/js/util.js

@@ -115,9 +115,11 @@
}

const redir = (id, term) => {
  // SPA navigation
  const shouldTrim = PRODUCTION && SEARCH_ENABLED
  const baseURLPrefix = shouldTrim ? "" : BASE_URL.replace(/\/$/g, "")
  const urlString = `${baseURLPrefix}${id}#:~:text=${encodeURIComponent(term)}/`
  window.Million.navigate(
    new URL(`${BASE_URL.replace(/\/$/g, "")}${id}#:~:text=${encodeURIComponent(term)}/`),
    new URL(urlString),
    ".singlePage",
  )
  closeSearch()
@@ -179,7 +181,7 @@
  })
}

const displayResults = (finalResults, extractHighlight = false) => {
const displayResults = (term, finalResults, extractHighlight = false) => {
  const results = document.getElementById("results-container")
  if (finalResults.length === 0) {
    results.innerHTML = `<button class="result-card">