aboutsummaryrefslogtreecommitdiffhomepage
path: root/docs/genstd.sh
diff options
context:
space:
mode:
authorMarvin Borner2024-03-25 18:59:03 +0100
committerMarvin Borner2024-03-25 18:59:48 +0100
commit14e38ce378236cf54924b58396168c1e94f8e6b2 (patch)
treeecbbb75517695de8897a2a9c58aa1a97ec2546f5 /docs/genstd.sh
parentf8398804d351667a7b887b89f6f70c7d5c407d22 (diff)
Improved samples by adding links to problems
Diffstat (limited to 'docs/genstd.sh')
-rwxr-xr-xdocs/genstd.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/genstd.sh b/docs/genstd.sh
index e290063..f2c0dd4 100755
--- a/docs/genstd.sh
+++ b/docs/genstd.sh
@@ -22,7 +22,7 @@ for file in $files; do
ntests=$(grep -cP "^:test" "$file" || true)
links="$links\n<li><span class='com'>:import</span> <a href=$filename.html>$(basename "$name" .bruijn)</a> <span class='stats'>($ndefs definitions, $ntests tests)</span></li>"
awk 'NR==FNR { gsub("<", "\\&lt;", $0); gsub(">", "\\&gt;", $0); a[n++]=$0; next } /CONTENT/ { for (i=0;i<n;++i) print a[i]; next } 1' "$file" content.template >"std/$filename.html"
- sed -i -e "s@NAME@$name@g" "std/$filename.html"
+ sed -i -e "s@NAME@$name@g" -e "s@INFO@@g" "std/$filename.html"
tot_ndefs=$((tot_ndefs + ndefs))
tot_ntests=$((tot_ntests + ntests))