From 1e43786b4c60b0eb52d2a500987fc0395016e362 Mon Sep 17 00:00:00 2001
From: Nicolas George <nicolas.george@normalesup.org>
Date: Mon, 23 Apr 2012 14:12:23 +0200
Subject: [PATCH] print_options: warn that the files are generated.

---
 doc/print_options.c | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/doc/print_options.c b/doc/print_options.c
index 4283e6a86d..339b942fb8 100644
--- a/doc/print_options.c
+++ b/doc/print_options.c
@@ -112,6 +112,8 @@ int main(int argc, char **argv)
     if (argc < 2)
         print_usage();
 
+    printf("@c DO NOT EDIT THIS FILE!\n"
+           "@c It was generated by print_options.\n\n");
     if (!strcmp(argv[1], "format"))
         show_format_opts();
     else if (!strcmp(argv[1], "codec"))