2020-08-12 14:42:12 +02:00
|
|
|
#!/bin/bash
|
|
|
|
|
|
|
|
|
|
function move_output_to_dist {
|
2020-08-19 08:47:06 +02:00
|
|
|
find . -name "$1" -type f -print0 | xargs -0r mv -t /dist/
|
2020-08-12 14:42:12 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
|
|
# Create new directory
|
|
|
|
|
mkdir -p /dist
|
|
|
|
|
|
|
|
|
|
# Move generated files
|
|
|
|
|
move_output_to_dist "*.pdf"
|
|
|
|
|
|
|
|
|
|
tamarin_success "Done :-)"
|
