diff --git a/tools/build-doc.sh b/tools/build-doc.sh index cfeabd0..9c71b45 100644 --- a/tools/build-doc.sh +++ b/tools/build-doc.sh @@ -25,6 +25,7 @@ css_path=$output_path/$css_file cat >> $output_path/odoc.css < $css_path