chiark / gitweb /
documentation: remove dead code.
authorVladimír Vondruš <mosra@centrum.cz>
Wed, 17 Jul 2019 16:51:35 +0000 (18:51 +0200)
committerVladimír Vondruš <mosra@centrum.cz>
Thu, 18 Jul 2019 11:34:34 +0000 (13:34 +0200)
commit4177f237bc5465ca56d54780aa652b09adc22c1c
tree35996e6d64cd8ebeadbb2939b86eacd8db2aaf11
parenta8c86f3b884d9afacc383ac1464738adf5ff11e2
documentation: remove dead code.
documentation/search.js