From 3e185d24c9fe772c7cf03d5475247fb829a21dfa Mon Sep 17 00:00:00 2001
From: Ivan Blinkov <github@blinkov.ru>
Date: Fri, 3 Apr 2020 17:15:22 +0300
Subject: [PATCH] Update docs.js

---
 website/js/docs.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/website/js/docs.js b/website/js/docs.js
index 7438f5a587..879fbdbca3 100644
--- a/website/js/docs.js
+++ b/website/js/docs.js
@@ -87,8 +87,8 @@ $(document).ready(function () {
                 hitsPerPage: 25,
                 'facetFilters': [
                     'lang:' + $('html').attr('lang'),
-                    'version' + $('html').attr('data-version'),
-                    'single-page' + $('html').attr('single-page'),
+                    'version:' + $('html').attr('data-version'),
+                    'single-page:' + $('html').attr('single-page'),
                 ]
             },
             debug: true
-- 
GitLab