From 2f7566090f932d509ad73510eb89654152fd5be0 Mon Sep 17 00:00:00 2001
From: moodler <moodler>
Date: Wed, 1 Jan 2003 11:26:50 +0000
Subject: [PATCH] Necessary file for documentation to work!

---
 lang/en/docs/files.php | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 lang/en/docs/files.php

diff --git a/lang/en/docs/files.php b/lang/en/docs/files.php
new file mode 100644
index 0000000000..85af408ef6
--- /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";
+
+
+?>
-- 
2.39.5