diff options
Diffstat (limited to 'reproduce/software/shell/configure.sh')
| -rwxr-xr-x | reproduce/software/shell/configure.sh | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/reproduce/software/shell/configure.sh b/reproduce/software/shell/configure.sh index 24e8409..219b335 100755 --- a/reproduce/software/shell/configure.sh +++ b/reproduce/software/shell/configure.sh @@ -1224,6 +1224,19 @@ if ! [ -d "$texbdir" ]; then mkdir "$texbdir"; fi tikzdir="$texbdir"/tikz if ! [ -d "$tikzdir" ]; then mkdir "$tikzdir"; fi +# If 'tex/build' and 'tex/tikz' aren't symbolic links, then we are in the +# tarball (not the Git repository), so we'll give them another name and let +# the script continue normally. +if rm -f tex/build; then + rm -f tex/tikz +else + mv tex/tikz tex/tikz-from-tarball + mv tex/build tex/build-from-tarball +fi + + + + # If 'tex/build' and 'tex/tikz' are symbolic links then 'rm -f' will delete # them and we can continue. However, when the project is being built from |