From 190cda5085ad2194883c09dafca70d550a611ff4 Mon Sep 17 00:00:00 2001
From: Jiri Kalvoda <jirikalvoda@kam.mff.cuni.cz>
Date: Wed, 24 May 2023 22:45:34 +0200
Subject: [PATCH] bashrc
---
bashrc | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)
create mode 100644 bashrc
diff --git a/bashrc b/bashrc
new file mode 100644
index 000000000..1c839d76f
--- /dev/null
+++ b/bashrc
@@ -0,0 +1,27 @@
+workdir_set()
+{
+ export workdir=$1
+ export LOGFILE=$workdir/log
+ PS1="$PS1[$workdir] "
+}
+
+workdir_mk()
+{
+ workdir=$(mktemp -d workdir-XXXXX)/
+ touch $workdir/log
+ workdir_set $workdir
+ echo ". bashrc && workdir_set $workdir"
+}
+
+workdir_commmit()
+{
+ if [[ "$workdir" == "" ]]
+ then
+ echo No workdir!
+ return 1
+ fi
+ cat $workdir/log >> log
+ rm $workdir/log
+ mv $workdir old_$workdir
+ unset $workdir
+}
--
GitLab