diff options
Diffstat (limited to 'config.fish')
| -rw-r--r-- | config.fish | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/config.fish b/config.fish index fcce7ae..480eb3f 100644 --- a/config.fish +++ b/config.fish @@ -42,6 +42,10 @@ set -x GPG_TTY (tty) if [ -d "$HOME/.local/bin" ] set -x PATH $PATH "$HOME/.local/bin" end +if [ -d "/opt/cuda/" ] + set -x CUDA_HOME "/opt/cuda" +end + if [ -d "$NPM_PACKAGES/bin" ] set -x PATH $PATH "$NPM_PACKAGES/bin" end @@ -61,6 +65,8 @@ if [ -d "$DOTNET_TOOLS_PATH" ] set -x PATH $PATH "$DOTNET_TOOLS_PATH" end + + if [ -d "$LEAN_PATH" ] set -x PATH $PATH "$LEAN_PATH" end |