2022-05-04 10:52:07 +02:00
|
|
|
#!/bin/bash
|
2022-07-26 20:13:04 +02:00
|
|
|
|
|
|
|
|
new_pwd=$(dirname $(realpath $0))
|
|
|
|
|
cd $new_pwd
|
|
|
|
|
|
|
|
|
|
# remove old data, if exists
|
|
|
|
|
if [ -d "tool_repos" ]
|
|
|
|
|
then
|
|
|
|
|
echo "Removing old tool_repos"
|
|
|
|
|
rm -Rf "tool_repos"
|
|
|
|
|
fi
|
|
|
|
|
|
|
|
|
|
echo "Initializing tool_repos"
|
|
|
|
|
mkdir -p tool_repos/uninitialized.git
|
|
|
|
|
git init --bare tool_repos/initialized.git
|
|
|
|
|
|
