panglesd / odoc / 982

73%

master: 56%

Build Type

push

github

Committed by panglesd

Commit Message

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

Run Details

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

10 existing lines in 1 file now uncovered.

10164 of 13926 relevant lines covered (72.99%)

2989.41 hits per line