diff -r 3d1cd23f88f7 -r 79eeb33c738f src/main/resources/make/uwproj.xsd
--- a/src/main/resources/make/uwproj.xsd Thu Nov 13 18:46:08 2025 +0100
+++ b/src/main/resources/make/uwproj.xsd Fri Nov 14 15:09:37 2025 +0100
@@ -228,7 +228,9 @@
Declares a configuration option.
The option argument name is specified with the arg attribute.
- Then, the children of this element specify possible values by defining the conditions
+ Optionally, a description for the help text of the resulting configure script can be specified by
+ a desc element.
+ Then, the next children of this element specify possible values by defining the conditions
(in terms of dependencies) and effects (in terms of defines and make variables) of each value.
Finally, a set of defaults is specified which supposed to automagically select the most
appropriate value for a specific platform under the available dependencies (in case the option is not
@@ -236,6 +238,7 @@
+