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-13 14:52:20 +03:00
|
|
|
make website-assets
|
2020-05-05 18:04:53 +03:00
|
|
|
|
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/
|
2020-05-25 20:07:55 +03:00
|
|
|
scp examples/us_tax_code/us_tax_code.html $1/
|
2020-05-17 20:13:50 +03:00
|
|
|
scp examples/tutorial/tutorial_en.html $1/
|
2020-05-06 16:35:43 +03:00
|
|
|
scp grammar.html $1/
|
|
|
|
|
scp catala.html $1/
|
2020-12-24 13:41:29 +03:00
|
|
|
scp _build/default/src/catala.bc.js $1/playground/
|
