doc/print_options: Move options headers to a saner place
authorDiego Biurrun <diego@biurrun.de>
Thu, 1 Aug 2013 12:41:34 +0000 (14:41 +0200)
committerDiego Biurrun <diego@biurrun.de>
Fri, 2 Aug 2013 17:19:02 +0000 (19:19 +0200)
commit79be2c325c5ee8f7ac9e28399e51986ebe99bb3c
tree94e970921e7bb24e0c3bd322385cdf6434754e96
parentb5a138652ff8a5b987d3e1191e67fd9f6575527e
doc/print_options: Move options headers to a saner place
doc/print_options.c