gen_docu: output 'None' for an empty flags list
authorMatthias Braun <matthias.braun@kit.edu>
Fri, 15 Jun 2012 09:26:24 +0000 (11:26 +0200)
committerMatthias Braun <matthias.braun@kit.edu>
Fri, 15 Jun 2012 10:57:47 +0000 (12:57 +0200)
commit4c1ef8f38f1c7fc64c7ac0ba1110cb87f8714bfd
tree2a45ea5f67ecde3fb0eeabf6141a6bf00009cea6
parentcee5f8c97c6fc342e533c802fd1f12ae288460ac
gen_docu: output 'None' for an empty flags list
scripts/gen_docu.py