chore(npins): Update #165

Merged
thubrecht merged 5 commits from npins-update into main 2024-11-19 01:11:41 +01:00
Showing only changes of commit a50637d55e - Show all commits

View file

@ -10,7 +10,7 @@ let
# - push to a new branch dgn-v0.A.B where A.B is the new version
# - finally, update the commit hash of the customization patch
dgn-id = "8f19cb1c9623f8da71f6512c1528d83acc35db57";
dgn-id = "d73e347b1cefe23092bfcb2d3f8a23903410203e";
port = 8084;
in