(* Always generate this file last, and unconditionally. It's used
* by the Makefile to know when we must re-run the generator.
(* Always generate this file last, and unconditionally. It's used
* by the Makefile to know when we must re-run the generator.