From a277ee4162bbe4e56b0cb7206595c4ca8416fc2c Mon Sep 17 00:00:00 2001 From: Klaus Aehlig Date: Fri, 22 Apr 2022 12:53:32 +0200 Subject: rule ["CC", "header directory"]: drop ill-advised "public stage" The idea, as documented, of a header directory is to have a directory, closed as a tree, owned by the respective library and internally handled in an efficient way (as a single tree). If we open up that directory, we just have staged data, and therefore should treat it as such. --- CC/RULES | 22 ++++------------------ 1 file changed, 4 insertions(+), 18 deletions(-) (limited to 'CC') diff --git a/CC/RULES b/CC/RULES index 81140cb..d687bf3 100644 --- a/CC/RULES +++ b/CC/RULES @@ -107,18 +107,13 @@ , "efficiently by the tool." ] , "target_fields": ["hdrs"] - , "string_fields": ["stage", "public stage"] + , "string_fields": ["stage"] , "field_doc": { "hdrs": ["The header files to be put into the header directory."] , "stage": [ "The location of the header directory." , "Path segments are joined with \"/\"." ] - , "public stage": - [ "If non-empty, no closure for the header directory's stage is created, " - , "so can be combined with other header directories having the same " - , "public staging directory." - ] } , "expression": { "type": "let*" @@ -141,18 +136,9 @@ } ] , [ "dir" - , { "type": "if" - , "cond": {"type": "FIELD", "name": "public stage"} - , "then": - { "type": "to_subdir" - , "subdir": {"type": "var", "name": "stage"} - , "$1": {"type": "var", "name": "hdrs"} - } - , "else": - { "type": "singleton_map" - , "key": {"type": "var", "name": "stage"} - , "value": {"type": "TREE", "$1": {"type": "var", "name": "hdrs"}} - } + , { "type": "singleton_map" + , "key": {"type": "var", "name": "stage"} + , "value": {"type": "TREE", "$1": {"type": "var", "name": "hdrs"}} } ] ] -- cgit v1.2.3