diff options
| -rwxr-xr-x | makediffhtml.sh | 2 | ||||
| -rwxr-xr-x | makediffpdf.sh | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/makediffhtml.sh b/makediffhtml.sh index 15c4a30..f8f8783 100755 --- a/makediffhtml.sh +++ b/makediffhtml.sh @@ -1,6 +1,6 @@ #!/bin/sh -./makediff.sh virtio-html.tex +./makediff.sh virtio-html.tex || exit 3 SPECDOC=${SPECDOC:-`cat REVISION`} SPECDOC="${SPECDOC}-diff" diff --git a/makediffpdf.sh b/makediffpdf.sh index c7864df..b3031c4 100755 --- a/makediffpdf.sh +++ b/makediffpdf.sh @@ -1,5 +1,5 @@ #make pdf diff using latexpand and latexdiff-fast -./makediff.sh virtio.tex +./makediff.sh virtio.tex || exit 3 SPECDOC=${SPECDOC:-`cat REVISION`} SPECDOC="${SPECDOC}-diff" rm $SPECDOC.aux $SPECDOC.pdf $SPECDOC.out |