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 593b1d9..6ffb4ff 100755 --- a/reproduce/software/shell/configure.sh +++ b/reproduce/software/shell/configure.sh @@ -1081,6 +1081,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 |