Driver: uniformize names for _odoc dir
`odoc_dir` was sometimes used to refer to the root of the directory containing
.odoc files (`_odoc` by default), and sometimes used to refer to the direct
parent of a `.odoc` file.
The root of the directory containing `.odoc` files was referred as `odoc_dir`,
`output_dir`.
The root of the directory containing `.odocl` files was referred as `odocl_dir`,
`link_dir`, `linked_dir`.
This commit cleans that. The root of the directory for `.odoc` files is
consistently named `odoc_dir`, the root for `.odocl` files is
`odocl_dir`.
3addbf
-
Nov 05 22:30 +00:00