We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent ebaab83 commit 87c0287Copy full SHA for 87c0287
.devcontainer/conf/shell/var/tmp/snippets/rc.sh
@@ -1,6 +1,6 @@
1
2
-# remove potentially appended $HOME/.local/bin from PATH
3
-PATH="${PATH%:$HOME/.local/bin}"
+# remove potentially present $HOME/.local/bin from PATH
+PATH="${PATH/:$HOME\/.local\/bin/}"
4
5
# set PATH so it includes user's private bin if it exists
6
if [ -d "$HOME/bin" ] && [[ "$PATH" != *"$HOME/bin"* ]] ; then
.devcontainer/devcontainer.json
@@ -5,7 +5,7 @@
"args": {
"GHC_VERSION": "9.10.2",
7
// "SUBTAG": "int-native",
8
- "HLS_VERSION": "2.11.0.0",
+ "HLS_VERSION": "2.12.0.0",
9
"USE_ZSH_FOR_ROOT": "unset-to-use-ash",
10
"LANG": "C.UTF-8",
11
"TZ": ""
0 commit comments