catala/generate_website_assets.sh

33 lines
1.7 KiB
Bash
Raw Normal View History

2020-05-05 18:04:53 +03:00
#! /usr/bin/env bash
cd "$(dirname "$0")"
if [[ $1 == "" ]]; then
echo "USAGE: $1 DST where DST is the directory in which files have to be copied"
exit 1
fi
2020-05-25 20:13:09 +03:00
rsync -a _build/default/_doc/_html/ $1/ocaml_docs/
2020-05-06 16:35:43 +03:00
scp examples/allocations_familiales/allocations_familiales.html $1/
scp examples/us_tax_code/us_tax_code.html $1/
2020-12-24 18:09:40 +03:00
scp examples/tutorial_en/tutorial_en.html $1/
scp examples/tutoriel_fr/tutoriel_fr.html $1/
2020-05-06 16:35:43 +03:00
scp grammar.html $1/
scp catala.html $1/
scp _build/default/src/catala_web/catala_web.bc.js $1/playground/
2020-12-25 19:09:44 +03:00
scp examples/tutorial_en/tutorial_en.catala_en $1/playground/
scp examples/tutoriel_fr/tutoriel_fr.catala_fr $1/playground/
2021-01-10 22:47:01 +03:00
cat examples/allocations_familiales/prologue.catala_fr > allocations_familiales.catala_fr
cat examples/allocations_familiales/decrets_divers.catala_fr >> allocations_familiales.catala_fr
cat examples/allocations_familiales/securite_sociale_L.catala_fr >> allocations_familiales.catala_fr
cat examples/allocations_familiales/securite_sociale_R.catala_fr >> allocations_familiales.catala_fr
cat examples/allocations_familiales/securite_sociale_D.catala_fr >> allocations_familiales.catala_fr
cat examples/allocations_familiales/epilogue.catala_fr >> allocations_familiales.catala_fr
cat examples/allocations_familiales/tests/tests_allocations_familiales.catala_fr >> allocations_familiales.catala_fr
sed -r '/^@@Inclusion.+$/d' allocations_familiales.catala_fr > allocations_familiales_fixed.catala_fr
mv -f allocations_familiales_fixed.catala_fr allocations_familiales.catala_fr
scp allocations_familiales.catala_fr $1/playground/
rm allocations_familiales.catala_fr
2020-12-25 19:09:44 +03:00
scp syntax_highlighting/en/ace/mode-catala_en.js $1/playground/
2021-01-10 22:47:01 +03:00
scp syntax_highlighting/fr/ace/mode-catala_fr.js $1/playground/