From 6fae25b305d714b3ab7608fa003f1af9bf024545 Mon Sep 17 00:00:00 2001
From: Hsieh Chin Fan <pham@topo.tw>
Date: Tue, 14 Feb 2023 13:33:23 +0800
Subject: Rename tools into bin

---
 tools/install.sh | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100755 tools/install.sh

(limited to 'tools/install.sh')

diff --git a/tools/install.sh b/tools/install.sh
deleted file mode 100755
index 1f1dd86..0000000
--- a/tools/install.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#! /usr/bin/env bash
-
-set -e
-
-# Default settings
-SETTING_DIR=${SETTING_DIR:-~/helper}
-REPO=${REPO:-typebrook/helper}
-REMOTE=${REMOTE:-https://github.com/${REPO}.git}
-BRANCH=${BRANCH:-dev}
-RCFILE=${RCFILE:-~/.$(basename $SHELL)rc}
-
-if [ ! -d $SETTING_DIR ]; then
-  git clone --depth=1 --branch "$BRANCH" "$REMOTE" "$SETTING_DIR" || {
-      error "git clone of helper repo failed"
-      exit 1
-  }
-fi
-
-# Write initial commands into .bashrc or .zshrc
-sed -i'.bak' "\^# $REPO^, /^$/ d" $RCFILE
-cat >>$RCFILE <<EOF
-
-# $REPO
-export SETTING_DIR=$SETTING_DIR
-source \$SETTING_DIR/tools/init/load-settings.sh
-EOF
-
-cd "$SETTING_DIR" || exit 1
-git swapprotocol
-make
-- 
cgit v1.2.3-70-g09d2