diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2025-05-12 16:57:56 +0200 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2025-05-12 16:57:56 +0200 |
commit | a575ef826eb054bc2236bf87a42adcf7a7674792 (patch) | |
tree | bc87a4cea2672b137e5d19641572959b821d5bf3 /reproduce | |
parent | df9e291826fbc7e717b40d2d07f1d7607a2f2455 (diff) |
Summary: will not affect existing configuration or analysis.
Until this commit, if the user gave the build directory interactively (had
not run './project configure' with '--build-dir'), the '.build' and
'.local' symbolic links were not created, resulting in a crash shortly
afterwards (when Maneage tried to write 'LOCAL.conf' in the build
directory!).
With this commit, the problem is solved by creating these links also when
the build directory is given interactively and after all the sanity checks
have passed.
Diffstat (limited to 'reproduce')
-rwxr-xr-x | reproduce/software/shell/configure.sh | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/reproduce/software/shell/configure.sh b/reproduce/software/shell/configure.sh index 4887816..1771487 100755 --- a/reproduce/software/shell/configure.sh +++ b/reproduce/software/shell/configure.sh @@ -1146,6 +1146,20 @@ EOF echo " ** Please select another directory." echo "" else + # Set the '.build' and '.local' symbolic links (and delete + # possibly existing symbolic links). These commands are also + # present in the top-level 'project' script, but they are only + # invoked when '--build-dir' is called. When it is not called + # (the user wants to insert the directories interactively: the + # scenario here), the links need to be created from + # scratch. Furthermore, in case the given directory to + # '--build-dir' has problems (fails to pass the sanity checks + # above), the symbolic links also need to be recreated. + rm -f .build .local + ln -s $bdir .build + ln -s $bdir/software/installed .local + + # Inform the user echo " -- Build directory set to ($instring): '$bdir'" fi done |