From 37d0ca9489f5b95b351346d26069bea99181f47a Mon Sep 17 00:00:00 2001 From: Tom Hubrecht Date: Tue, 8 Oct 2024 14:13:00 +0200 Subject: [PATCH] chore(dgsi): Update? --- npins/sources.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/npins/sources.json b/npins/sources.json index 7efe5be..6ad46d4 100644 --- a/npins/sources.json +++ b/npins/sources.json @@ -45,9 +45,9 @@ "url": "https://git.dgnum.eu/DGNum/dgsi.git" }, "branch": "main", - "revision": "9c4413faa1610167d65b5c6110cdbc714eb14887", + "revision": "129641cc1fdd657c070c54f3b93aa0cd7c5a5b1d", "url": null, - "hash": "0pn684dc1s5v3nqiy6jpxpr26mv5z6pq1i5cvza9d2hi7lddp3wb" + "hash": "0s4bkj7y6iqch8xislxyx7w5rn0xz95rvj9gfwcvm3p7sqj92ldj" }, "disko": { "type": "GitRelease",