3a977a94ca
- Makes the autocomplete results highlight with up/down arrows. - Allows you to unselect autocomplete results by using arrow keys. - Fixed a bug in previous commits where enter did not take you to autocomplete result. - Return now goes to the search page if no autocomplete result is selected. - Search results table now properly wraps. (It would be nice to make it wider but I wasn't able to). - Fixed a bug in the previous commit where docs were not showing, due to failure to copy a modified js file. |
||
|---|---|---|
| .. | ||
| LeanInk | ||
| Output | ||
| Process | ||
| LeanInk.lean | ||
| Load.lean | ||
| Output.lean | ||
| Process.lean | ||