What is our stand on using the name Linux or the name GNU/Linux. For those who do not know: the OS Linux was built by Linux Torvalds in 1991. He basically only built a kernel and used parts of the GNU project to pad it out to a complete OS. People started calling the whole OS Linux. At this the founder of GNU, Richard Stallman, balked, because he feels that the OS is as much his as Linus' and that he deserves credit for it. He would like to see that credit in the shape of the OS being called GNU/Linux rather than just Linux. I grepped the current stable CVS (well, that of a few weeks ago) and found that a few files (mostly of the documentation type) mention Linux instead of GNU/Linux. Should we change these instances to GNU/Linux? -- branko collin collin@xxxxxxxxx
