generalize the export script

This commit is contained in:
Laureηt 2024-01-02 12:01:58 +01:00
parent 3fb6028676
commit e5623592cc
Signed by: Laurent
SSH key fingerprint: SHA256:kZEpW8cMJ54PDeCvOhzreNr4FSh6R13CMGH/POoO8DI
2 changed files with 12 additions and 9 deletions

View file

@ -33,6 +33,10 @@ function export_html(notebook_path, html_path)
end end
end end
# TODO: use loop cli args # get cli args
export_html("exos.jl", "exos.html") for arg in ARGS
export_html("index.jl", "index.html") filename, _ = splitext(arg)
html_path = filename * ".html"
println("Exporting $arg to $html_path")
export_html(arg, filename * ".html")
end

View file

@ -35,17 +35,16 @@
]; ];
buildPhase = '' buildPhase = ''
# TODO: comment this shit # copy the notebooks, Pluto needs write permission
cp $src/TP1/notebook.jl index.jl cp $src/TP1/notebook.jl index.jl
cp $src/TD/notebook.jl exos.jl cp $src/TD/notebook.jl exos.jl
chmod +w index.jl exos.jl chmod +w index.jl exos.jl
cp $src/export_html.jl export_html.jl # julia needs permission to create .julia directory
export HOME=$TMPDIR
# https://github.com/NixOS/nix/issues/670#issuecomment-1211700127 # run and export the notebooks
export HOME=$(pwd) julia $src/export_html.jl exos.jl index.jl
julia export_html.jl
''; '';
installPhase = '' installPhase = ''