Recorded after the fact from commit 0e4fe0a.
Context
The first docs tree needed a search box before any other part of Inside had one.
Decision
The docs top bar searched inside/docs/search.json only, and Enter opened the first hit.
Consequences
Inside had a second search box over the map, so there were two boxes over two indexes, and Enter could open a page the reader had not chosen. Replaced by ADR-0012.