diff options
Diffstat (limited to 'reproduce/software/shell/bashrc.sh')
-rwxr-xr-x | reproduce/software/shell/bashrc.sh | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/reproduce/software/shell/bashrc.sh b/reproduce/software/shell/bashrc.sh index 6bb871b..3e496c0 100755 --- a/reproduce/software/shell/bashrc.sh +++ b/reproduce/software/shell/bashrc.sh @@ -28,6 +28,11 @@ # When doing the project's analysis: all software have known # versions. # +# shell +# ----- +# When the user has activated the interactive shell (with './project +# shell'). +# # # Copyright (C) 2019-2022 Mohammad Akhlaghi <mohammad@akhlaghi.org> # @@ -43,3 +48,48 @@ # # You should have received a copy of the GNU General Public License # along with this script. If not, see <http://www.gnu.org/licenses/>. + + + + + +# Interactive mode settings. We don't want these within the pipeline +# because they are useless there (for example the introduction message or +# prompt) and can un-necessarily slow down the running jobs (recall that +# the shell is executed at the start of each recipe). +if [ x$PROJECT_STATUS = xshell ]; then + + # A small introductory message. + echo "----------------------------------------------------------------------" + echo "Welcome to the Maneage interactive shell for this project, running" + echo " $(sh --version | awk 'NR==1')" + echo + echo "This shell's home directory is the project's build directory:" + echo " HOME: $HOME" + echo + echo "This shell's startup file is in the project's source directory:" + echo " $PROJECT_RCFILE" + echo + echo "To return to your host shell, run the 'exit' command." + echo "----------------------------------------------------------------------" + + # To activate colors in generic commands. + alias ls='ls --color=auto' + alias grep='grep --color=auto' + + # Add the Git branch information to the command prompt only when Git is + # present. Also set the command-prompt color to purple for normal users + # and red when the root is running it. + if git --version &> /dev/null; then + parse_git_branch() { + git branch 2> /dev/null | sed -e '/^[^*]/d' -e 's/* \(.*\)/ (\1)/' + } + else + parse_git_branch() { echo &> /dev/null; } + fi + if [ x$(whoami) = xroot ]; then + export PS1="[\[\033[01;31m\]\u@\h \W\[\033[32m\]\$(parse_git_branch)\[\033[00m\]]# " + else + export PS1="[\[\033[01;35m\]maneage@\h \W\[\033[32m\]\$(parse_git_branch)\[\033[00m\]]$ " + fi +fi |