diff options
author | ache <ache@ache.one> | 2023-02-26 01:18:15 +0100 |
---|---|---|
committer | ache <ache@ache.one> | 2023-02-26 01:18:15 +0100 |
commit | b035c6992fe6582ed8ba90a0259655c26ff93995 (patch) | |
tree | 51cae36ae3783b549696c524ae53dec9673e40fe /config.fish | |
parent | Use type instead of which (diff) |
Configur Lean
Diffstat (limited to 'config.fish')
-rw-r--r-- | config.fish | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/config.fish b/config.fish index 4485a78..466922e 100644 --- a/config.fish +++ b/config.fish @@ -22,6 +22,12 @@ if type ruby 2> /dev/null > /dev/null set RUBY_PATH (ruby -e 'print Gem.user_dir')/bin end +if test -e /home/ache/.elan/ + set LEAN_PATH /home/ache/.elan/bin +end + + + set -x NPM_PACKAGES "$HOME/.npm-packages" set -x GOPATH "$HOME/.go" set -x NODE_PATH "$NPM_PACKAGES/lib/node_modules:$NODE_PATH" @@ -50,6 +56,10 @@ end if [ -d "$EMSCRIPTEN_PATH" ] set -x PATH $PATH "$EMSCRIPTEN_PATH" end + +if [ -d "$LEAN_PATH" ] + set -x PATH $PATH "$LEAN_PATH" +end if [ -d "$DEVKITPRO_DIR" ] set -x DEVKITPRO '/opt/devkitpro' set -x DEVKITARM '/opt/devkitpro/devkitARM' |