waveterm/dev.commandline.waveterm
0
0
Fork 0
mirror of https://github.com/wavetermdev/dev.commandline.waveterm.git synced 2026-04-22 15:27:29 -07:00
Code Issues Packages Projects Releases Wiki Activity

Add PHP7.3 SDK (#94)

Browse Source
This commit is contained in:
Daniel Smith
2019-08-02 23:51:17 +12:00
committed by eszlari
parent 495d95d691
commit 830310b45b
1 changed files with 4 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
code.sh
+4
View File
@@ -17,5 +17,9 @@ if [[ -d /usr/lib/sdk/node10 ]]; then
. /usr/lib/sdk/node10/enable.sh
fi
if [[ -d /usr/lib/sdk/php73 ]]; then
. /usr/lib/sdk/php73/enable.sh
fi
exec env PATH="${PATH}:${XDG_DATA_HOME}/node_modules/bin" \
/app/extra/vscode/bin/code --extensions-dir=${XDG_DATA_HOME}/vscode/extensions "$@" ${WARNING_FILE}