diff --git a/BitKeeper/etc/logging_ok b/BitKeeper/etc/logging_ok
index 6646091223b..36c31361722 100644
--- a/BitKeeper/etc/logging_ok
+++ b/BitKeeper/etc/logging_ok
@@ -47,3 +47,4 @@ tonu@x3.internalnet
 venu@work.mysql.com
 zak@linux.local
 jcole@mugatu.spaceapes.com
+arjen@fred.bitbike.com
diff --git a/Docs/include.de.texi b/Docs/include.de.texi
deleted file mode 100644
index 228bf7d6c86..00000000000
--- a/Docs/include.de.texi
+++ /dev/null
@@ -1,3 +0,0 @@
-@c This file is autogenerated by the Makefile
-@set mysql_version 4.0.2
-@set default_port 3306