Necessary file for documentation to work!

diff --git a/lang/en/docs/files.php b/lang/en/docs/files.php
new file mode 100644 (file)
index 0000000..85af408
--- /dev/null
+++ b/lang/en/docs/files.php
@@ -0,0 +1,18 @@
+<?PHP // $Id$
+      // Names of the documentation files
+
+$string['intro.html'] = "Introduction";
+$string['background.html'] = "Background";
+$string['features.html'] = "Features";
+$string['release.html'] = "Release Notes";
+$string['install.html'] = "Installation";
+$string['upgrade.html'] = "Upgrading";
+$string['teacher.html'] = "Teacher Manual";
+$string['developer.html'] = "Developer Manual";
+$string['cvs.html'] = "Using CVS";
+$string['future.html'] = "Future";
+$string['credits.html'] = "Credits";
+$string['licence.html'] = "License";
+
+
+?>