# HG changeset patch
# User wenzelm
# Date 982007239 -3600
# Node ID 5ceaa79c220d4770b621f14bad0e283f1089beda
# Parent  014e7b5c77ba38ea8e3a42badc317752dcb83b1a
tuned;

diff -r 014e7b5c77ba -r 5ceaa79c220d src/HOL/Unix/document/root.tex
--- a/src/HOL/Unix/document/root.tex	Mon Feb 12 20:45:12 2001 +0100
+++ b/src/HOL/Unix/document/root.tex	Mon Feb 12 20:47:19 2001 +0100
@@ -189,7 +189,7 @@
 to clean up the situation.  In Unix \texttt{root} may perform any file-system
 operation without any access control limitations.\footnote{This is the typical
   Unix way of handling abnormal situations: while it is easy to run into odd
-  cases due to simplistic policies it as well quite easy to get out.  There
+  cases due to simplistic policies it is as well quite easy to get out.  There
   are other well-known systems that make it somewhat harder to get into a fix,
   but almost impossible to get out again!}