Merge branch 'dev' into gentoo

fix: COQBIN env variable
This commit is contained in:
David JULIEN 2021-10-19 17:25:46 +02:00
commit 72b13bc4d9
No known key found for this signature in database
GPG Key ID: 4B388E8BD9D47382
1 changed files with 1 additions and 1 deletions

View File

@ -23,7 +23,7 @@ export GTK2_RC_FILES="$XDG_CONFIG_HOME/gtk-2.0/gtkrc-2.0"
export TEXMFHOME="$XDG_DATA_HOME/texmf"
export CARGO_HOME="$XDG_DATA_HOME/cargo"
export OPAMROOT="$XDG_DATA_HOME/opam"
export COQBIN="$OPAMROOT/default/bin"
export COQBIN="$OPAMROOT/default/bin/"
## default programs
export GPG_ASKPASS="/usr/bin/pinentry-curses"