Skip to content

Commit

Permalink
docs: quote args in src/docs/copy.sh
Browse files Browse the repository at this point in the history
  • Loading branch information
erooke committed Nov 12, 2024
1 parent e37880d commit 548347e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/doc/copy.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ html_path=../../_doc/_html
# get name of internal library
lib_name=$(ls $html_path | grep kind2dev)
# copy ./include dir into library documentation dir
cp -r ./include $html_path/$lib_name
cp -r ./include "$html_path/$lib_name"
# compile index.mld into page-index.odoc file
odoc compile --pkg=$lib_name index.mld
odoc compile --pkg="$lib_name" index.mld
# convert page-index.odoc to index.html and resolve links to other webpages
odoc html ./page-index.odoc -I ../.kind2dev.objs/byte --output $html_path
# replace all instances of kind2 with lib_name
Expand Down

0 comments on commit 548347e

Please sign in to comment.