From d69a79b03b8f2853b60773e38553d662a01ac269 Mon Sep 17 00:00:00 2001
From: Tim Schumacher <timschumi@gmx.de>
Date: Sun, 5 Jun 2022 03:04:43 +0200
Subject: [PATCH] Ports: Automatically enter the work directory when running
 `dev`

---
 Ports/.port_include.sh | 2 ++
 1 file changed, 2 insertions(+)

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)"