chiark / gitweb /
make-directive-index: remove duplicated list of sections
authorZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
Tue, 15 Jan 2013 02:02:49 +0000 (21:02 -0500)
committerZbigniew Jędrzejewski-Szmek <zbyszek@in.waw.pl>
Tue, 15 Jan 2013 16:30:41 +0000 (11:30 -0500)
commiteeb019b5b5db785feb0666f3238b1240e7f3e42e
tree47458bd2fede87201297f45a677884e65c44c848
parent4a431c9ab1475b38868c9e240a5615739a3d6458
make-directive-index: remove duplicated list of sections
make-directive-index.py