Skip to content

Commit

Permalink
driver: Update to --home-breadcrumb new name
Browse files Browse the repository at this point in the history
Julow committed Dec 11, 2024
1 parent 7fa3d8b commit cd23ba8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/driver/odoc.ml
Original file line number Diff line number Diff line change
@@ -208,7 +208,7 @@ let html_generate ~output_dir ?sidebar ?(ignore_output = false)
empty search_uris
in
let cmd =
!odoc % "html-generate" % "--escape-breadcrumb" % p file %% index
!odoc % "html-generate" % "--home-breadcrumb" % p file %% index
%% search_uris % "-o" % output_dir
in
let cmd =

0 comments on commit cd23ba8

Please sign in to comment.