Commits on Nov 5, 2024

1. 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`.

   

   panglesd committed Nov 5, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for f739ad1
   • Browse repository at this point

   Copy the full SHA

   f739ad1 View commit details

   Browse the repository at this point in the history