From 8e6f6d694b8c183efc64c2dd7becbd2195303fd9 Mon Sep 17 00:00:00 2001
From: Ben Sima <ben@bsima.me>
Date: Tue, 26 Jul 2022 09:19:54 -0400
Subject: Put _/bin on the PATH

The motivation for this was to prevent `lint` from rebuilding every time I ran
it. That was really annoying.
---
 .envrc                   | 5 ++++-
 Biz/Ide/hooks/pre-commit | 2 +-
 Biz/Ide/lint             | 2 --
 3 files changed, 5 insertions(+), 4 deletions(-)
 delete mode 100755 Biz/Ide/lint

diff --git a/.envrc b/.envrc
index 228ed82..cdcae62 100644
--- a/.envrc
+++ b/.envrc
@@ -10,9 +10,12 @@
 #
   export BIZ_ROOT=$PWD
 #
-# tools for editing go here
+# scripts for editing go here
   PATH_add $BIZ_ROOT/Biz/Ide
 #
+# bild outputs go here
+  PATH_add $BIZ_ROOT/_/bin
+#
 # Biz/Dragons.hs:
   export GITHUB_CLIENT_ID=aa575dc96263bc99556d
   export GITHUB_CLIENT_STATE=$(cat /proc/sys/kernel/random/uuid)
diff --git a/Biz/Ide/hooks/pre-commit b/Biz/Ide/hooks/pre-commit
index 31a4e68..6978209 100755
--- a/Biz/Ide/hooks/pre-commit
+++ b/Biz/Ide/hooks/pre-commit
@@ -17,5 +17,5 @@
       echo "info:  version:  $ns:  $version"
     fi
   done
-  $BIZ_ROOT/Biz/Ide/lint **/*
+  lint **/*
 ##
diff --git a/Biz/Ide/lint b/Biz/Ide/lint
deleted file mode 100755
index f8bcc1e..0000000
--- a/Biz/Ide/lint
+++ /dev/null
@@ -1,2 +0,0 @@
-#!/usr/bin/env bash
-bild $BIZ_ROOT/Biz/Lint.hs && $BIZ_ROOT/_/bin/lint $@
-- 
cgit v1.2.3