panglesd / odoc / 981

73%

master: 56%

push

github

Sidebar: better handling of missing page index

We use the id name (corresponding to the directory name) for the page title.

There is one case where we don't have access to an id:
```
$ odoc compile --output_dir _odoc --parent-id "" file.mld
$ odoc link _odoc/page-file.mld
$ odoc sidebar-generate -P _odoc/
```

The parent id of page `file` is `None` and we do not have an `index.mld` with
the same parent...

See also the test

19 of 20 new or added lines in 1 file covered. (95.0%)

10164 of 13926 relevant lines covered (72.99%)

2989.42 hits per line