diff options
author | Thomas Schwinge <tschwinge@gnu.org> | 2006-12-04 19:42:27 +0000 |
---|---|---|
committer | Thomas Schwinge <tschwinge@gnu.org> | 2006-12-04 19:42:27 +0000 |
commit | 576122f6309c49745d16be06e7ce2218a769e96c (patch) | |
tree | bc49eff8ff2c6f5f8a27b76cab451855ee7f2b3f /hurd-paper.html | |
parent | aa6ec7c28582d02dc59e7ce57315126b4925fd93 (diff) |
This was a `sed'-based change, where I didn't review every single detail and
thus hope that I didn't break anything. Replace `MiG' with `MIG'. Replace
`MIG' with `GNU MIG' and `The GNU Hurd' with `GNU Hurd' when linking to the
pages. Make the space between `GNU' and `Hurd' or `Mach' or `MIG'
non-breakable.
Diffstat (limited to 'hurd-paper.html')
-rw-r--r-- | hurd-paper.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/hurd-paper.html b/hurd-paper.html index fbd34014..19ccef2f 100644 --- a/hurd-paper.html +++ b/hurd-paper.html @@ -120,7 +120,7 @@ But the wall between user and system remains; no user can cross it without special privilege. <P> -The GNU Hurd, by contrast, is designed to make the area of +The GNU Hurd, by contrast, is designed to make the area of <STRONG>system</STRONG> code as limited as possible. |