From e37880d455c84e9fc942749e4d12ec2a99fbd6c0 Mon Sep 17 00:00:00 2001 From: Ethan Rooke Date: Tue, 12 Nov 2024 10:28:47 -0600 Subject: [PATCH 1/2] docs: make src/docs/copy.sh shebang more portable `/bin/bash` is not guaranteed to exist on all systems. Replacing the shebang with `/usr/bin/env bash` looks up the location of bash on such systems. --- src/doc/copy.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/doc/copy.sh b/src/doc/copy.sh index 25b372fd8..9abf7e1ae 100755 --- a/src/doc/copy.sh +++ b/src/doc/copy.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash html_path=../../_doc/_html # get name of internal library lib_name=$(ls $html_path | grep kind2dev) From 548347e8af0b99d057428e16d11525b1e620d6c0 Mon Sep 17 00:00:00 2001 From: Ethan Rooke Date: Tue, 12 Nov 2024 11:07:38 -0600 Subject: [PATCH 2/2] docs: quote args in src/docs/copy.sh --- src/doc/copy.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/doc/copy.sh b/src/doc/copy.sh index 9abf7e1ae..b58293c51 100755 --- a/src/doc/copy.sh +++ b/src/doc/copy.sh @@ -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