docs: Debian and Ubuntu are now separate distros.
authorRichard Jones <rjones@redhat.com>
Mon, 15 Nov 2010 22:20:51 +0000 (22:20 +0000)
committerRichard W.M. Jones <rjones@redhat.com>
Thu, 18 Nov 2010 11:37:23 +0000 (11:37 +0000)
commit4940b7cf528585ad896b13eea7f369dd55bc992e
treeb3661ccd0eda7e7ff4190d6614ca68c4c37583c8
parent8838ba052689bd41dc2259b8ef36394199d06b20
docs: Debian and Ubuntu are now separate distros.
(cherry picked from commit 47af6aaab8f2dde736951b4e549c2638d942dae5)
generator/generator_actions.ml