Thanks for adding this. Please push.
Chris
On 9/9/2022 3:18 pm, Sebastian Huber wrote:
> Update #4560.
> ---
> user/rsb/project-sets.rst | 9 +
> 1 file changed, 9 insertions(+)
>
> diff --git a/user/rsb/project-sets.rst b/user/rsb/project-sets.rst
> index 54a3f8e..ce839c5 100644
> ---
Update #4560.
---
user/rsb/project-sets.rst | 9 +
1 file changed, 9 insertions(+)
diff --git a/user/rsb/project-sets.rst b/user/rsb/project-sets.rst
index 54a3f8e..ce839c5 100644
--- a/user/rsb/project-sets.rst
+++ b/user/rsb/project-sets.rst
@@ -116,6 +116,15 @@ build sets:
``--with-ob
