From ca57d67ec9e3f45060564da43780197aef714a56 Mon Sep 17 00:00:00 2001 From: Max Horn Date: Thu, 14 Apr 2022 13:23:45 +0200 Subject: [PATCH] Improve some 'do not edit this file' comments --- doc/ref/intrfc.xml | 2 -- doc/versiondata | 8 ++++++-- doc/versiondata.in | 8 ++++++-- etc/ffgen.c | 3 ++- 4 files changed, 14 insertions(+), 7 deletions(-) diff --git a/doc/ref/intrfc.xml b/doc/ref/intrfc.xml index 91d620c41e..cadc9b3174 100644 --- a/doc/ref/intrfc.xml +++ b/doc/ref/intrfc.xml @@ -1,5 +1,3 @@ - - diff --git a/doc/versiondata b/doc/versiondata index b0d3cfce1a..32aaf93d47 100644 --- a/doc/versiondata +++ b/doc/versiondata @@ -1,5 +1,9 @@ - + diff --git a/doc/versiondata.in b/doc/versiondata.in index 73b0c9c332..8f4647556e 100644 --- a/doc/versiondata.in +++ b/doc/versiondata.in @@ -1,5 +1,9 @@ - + diff --git a/etc/ffgen.c b/etc/ffgen.c index 569b194900..ce4fdd0322 100644 --- a/etc/ffgen.c +++ b/etc/ffgen.c @@ -56,7 +56,8 @@ unsigned int needed_bits(unsigned int x) void emit_code(FILE * dest, int header) { unsigned i, j; - fprintf(dest, "/* This file is generated by etc/ffgen.c during build do not edit */\n"); + fprintf(dest, "/* This file has been generated by etc/ffgen.c during build,\n"); + fprintf(dest, " do not edit */\n"); if (header) { fprintf(dest, "#ifndef GAP_FFDATA_H\n"); fprintf(dest, "#define GAP_FFDATA_H\n");