Discussion:
"search history" functionality
Vincent Lefevre
2018-02-04 18:05:00 UTC
Permalink
There is an extraneous space before "History", i.e. yielding 2 spaces
instead of one, or was it added on purpose?

Attached proposed patch to remove this space.
--
Vincent Lefèvre <***@vinc17.net> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
Kevin J. McCarthy
2018-02-04 19:06:36 UTC
Permalink
Post by Vincent Lefevre
There is an extraneous space before "History", i.e. yielding 2 spaces
instead of one, or was it added on purpose?
Attached proposed patch to remove this space.
Whoops, that was indeed a mistake. Thanks Vincent. Feel free to push
the fix, otherwise I will do it later on today.

-Kevin
--
Kevin J. McCarthy
GPG Fingerprint: 8975 A9B3 3AA3 7910 385C 5308 ADEF 7684 8031 6BDA
Loading...