web/repo: the file filter keeps the tree's height and says when nothing loaded matches, so filtering doesn't move the page

49fa86f2 parent 000899f5 +19 −1
browse files