Utiliser le script de build et les répertoires output pour la documentation
This commit is contained in:
parent
5d6e2e7b1a
commit
066815bc53
@ -1,5 +1,5 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
pushd /src
|
||||
make build
|
||||
build
|
||||
popd
|
||||
|
@ -1,14 +1,13 @@
|
||||
#!/bin/bash
|
||||
|
||||
function move_output_to_dist {
|
||||
find . -name "$1" -type f -print0 | xargs -0r mv -t /dist/
|
||||
}
|
||||
|
||||
# Create new directory
|
||||
mkdir -p /dist
|
||||
|
||||
# Move generated files
|
||||
move_output_to_dist "*.pdf"
|
||||
pushd /src
|
||||
mv ./output_public /dist/public
|
||||
mv ./output_private /dist/private
|
||||
popd
|
||||
|
||||
tamarin_success "Done :-)"
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user