2022-08-02 16:29:39 +02:00
|
|
|
#!/bin/bash
|
|
|
|
|
|
|
|
|
|
# Create new directory
|
|
|
|
|
mkdir -p /dist
|
|
|
|
|
|
|
|
|
|
# Move generated files
|
2022-08-08 11:51:55 +02:00
|
|
|
pushd /src
|
2022-08-11 09:00:15 +02:00
|
|
|
ls -l ./output_public
|
|
|
|
|
cp ./output_public/*.pdf /dist/public
|
|
|
|
|
cp ./output_private/*.pdf /dist/private
|
2022-08-08 11:51:55 +02:00
|
|
|
popd
|
2022-08-02 16:29:39 +02:00
|
|
|
|
|
|
|
|
tamarin_success "Done :-)"
|
|
|
|
|
|
