> I just committed a slightly modified patch in your name. Thank you very much Peter.
Christophe
- Re: Bug 9210: fix to replace Linux with GNU/Linux where n... Peter O'Gorman
- Re: Bug 9210: fix to replace Linux with GNU/Linux wh... Christophe Jarry
- Re: Bug 9210: fix to replace Linux with GNU/Linu... Peter O'Gorman
- Re: Bug 9210: fix to replace Linux with GNU/... Christophe Jarry
- Re: Bug 9210: fix to replace Linux with ... Ralf Wildenhues
- Re: Bug 9210: fix to replace Linux ... Christophe Jarry
- Re: Bug 9210: fix to replace Linux ... Christophe Jarry
- Re: Bug 9210: fix to replace Li... Bob Friesenhahn
- Re: Bug 9210: fix to replace Li... Christophe Jarry
- Re: Bug 9210: fix to replace Li... Peter O'Gorman
- Re: Bug 9210: fix to replace Li... Christophe Jarry
- Re: Bug 9210: fix to replace Linux ... Paolo Bonzini
