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
|
|
|
|
|
mv ./output_public /dist/public
|
|
|
|
|
mv ./output_private /dist/private
|
|
|
|
|
popd
|
2022-08-02 16:29:39 +02:00
|
|
|
|
|
|
|
|
tamarin_success "Done :-)"
|
|
|
|
|
|
