print_options: warn that the files are generated.
authorNicolas George <nicolas.george@normalesup.org>
Mon, 23 Apr 2012 12:12:23 +0000 (14:12 +0200)
committerNicolas George <nicolas.george@normalesup.org>
Mon, 23 Apr 2012 16:14:25 +0000 (18:14 +0200)
commit1e43786b4c60b0eb52d2a500987fc0395016e362
treea51b331842a0d23d4f74e89b67cf09bbc7bad840
parent9b84f8a987e7cd3bb966d065d50d79d453907bad
print_options: warn that the files are generated.
doc/print_options.c