Update with subsetting scripts
This commit is contained in:
@@ -34,11 +34,15 @@ cp -r $agdaHtml/* code/
|
||||
# Static folder changed, re-run Hugo
|
||||
hugo $hugoFlags --config=config.toml,config-urls.toml
|
||||
|
||||
# Output result
|
||||
mkdir $out
|
||||
cp -r public/$publicPath/* $out/
|
||||
|
||||
# Do post-processing of HTML files: render math and link up Agda code
|
||||
htmlfiles=$(find $out/ -regex "$out/.*\.html")
|
||||
# Do post-processing of HTML files: render math, link up Agda code, subset fonts and icons
|
||||
gendir="public/$publicPath"
|
||||
htmlfiles=$(find $gendir/ -regex "$gendir/.*\.html")
|
||||
chmod -R u+w $gendir
|
||||
echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./convert.rb --katex-js-file static/katex/katex.min.js
|
||||
echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./agda.rb
|
||||
echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./chatgpt-subset-feather-icon.rb $gendir/feather-sprite.svg
|
||||
echo $htmlfiles | xargs python3 chatgpt-subset-one-go.py $gendir
|
||||
|
||||
# Output result
|
||||
mkdir $out
|
||||
cp -r $gendir/* $out/
|
||||
|
||||
Reference in New Issue
Block a user