diff options
| -rwxr-xr-x | Ports/.port_include.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Ports/.port_include.sh b/Ports/.port_include.sh index 4bb4fc65d6..ee13ba0805 100755 --- a/Ports/.port_include.sh +++ b/Ports/.port_include.sh @@ -824,7 +824,9 @@ do_dev() { local first_hash="$(git -C "$git_repo" rev-list --max-parents=0 HEAD)" + pushd "$workdir" launch_user_shell + popd >/dev/null 2>&1 local current_hash="$(git -C "$git_repo" rev-parse HEAD)" |