diff options
Diffstat (limited to 'src/generator.ml')
| -rwxr-xr-x | src/generator.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/generator.ml b/src/generator.ml index df5ff7e2..766650f3 100755 --- a/src/generator.ml +++ b/src/generator.ml @@ -8712,3 +8712,10 @@ Run it from the top source directory using the command let close = output_to "src/MAX_PROC_NR" in generate_max_proc_nr (); close (); + + (* Always generate this file last, and unconditionally. It's used + * by the Makefile to know when we must re-run the generator. + *) + let chan = open_out "src/stamp-generator" in + fprintf chan "1\n"; + close_out chan |