Merge branch 'dev' into logos
fix: COQBIN env variable
This commit is contained in:
commit
3392b340d4
@ -20,7 +20,7 @@ export GTK2_RC_FILES="$XDG_CONFIG_HOME/gtk-2.0/gtkrc-2.0"
|
|||||||
export TEXMFHOME="$XDG_DATA_HOME/texmf"
|
export TEXMFHOME="$XDG_DATA_HOME/texmf"
|
||||||
export CARGO_HOME="$XDG_DATA_HOME/cargo"
|
export CARGO_HOME="$XDG_DATA_HOME/cargo"
|
||||||
export OPAMROOT="$XDG_DATA_HOME/opam"
|
export OPAMROOT="$XDG_DATA_HOME/opam"
|
||||||
export COQBIN="$OPAMROOT/default/bin"
|
export COQBIN="$OPAMROOT/default/bin/"
|
||||||
|
|
||||||
## default programs
|
## default programs
|
||||||
export SUDO_ASKPASS="$HOME/.local/bin/dmenupass"
|
export SUDO_ASKPASS="$HOME/.local/bin/dmenupass"
|
||||||
|
Reference in New Issue
Block a user