devel/copy_paper_to_web.sh at 72451510d96ab4897f9c277e49cd5d22a0d81c78

15 lines · 272 BBlame History Raw

1#!/bin/bash

3# Exit on error

4set -e

6# Get the directory containing this script

7cd "$(dirname "$0")/.."

9# First compile the paper

10./devel/compile_paper.sh

12# Then copy it to web-ui/public/

13cp paper/paper.pdf web-ui/public/

15echo "Paper copied to web-ui/public/paper.pdf"