Files
seL4/tools
Fennelfoxxo 162a38e865 Build: Allow optional output in config_gen.py
Previously, config_gen.py required the generated header and json to be
either written to a file or sent to stdout. This meant that there was
no way to avoid writing to a file, as the header and json data would be
merged into the same stdout stream. This change makes it so that the
header or json generation can be suppressed entirely by omitting the
corresponding --write-c or --write-json options.

Signed-off-by: James Martin <fennelfoxxo@gmail.com>
2025-04-27 11:33:45 +10:00
..
2025-04-14 12:05:16 +10:00
2020-06-18 12:39:46 +10:00
2025-04-14 12:05:16 +10:00
2025-04-14 12:05:16 +10:00
2025-02-26 17:11:57 +11:00
2025-04-14 12:05:16 +10:00
2025-02-26 17:11:57 +11:00
2025-04-14 12:05:16 +10:00