Fixed bug 812 about editing text files with backslashes in them.

diff --git a/files/index.php b/files/index.php
index df3213a63f020d9f292a98344989676f12adacac..2260d1bbb92132379391cca39762cc8466239abd 100644 (file)
--- a/files/index.php
+++ b/files/index.php
@@ -335,7 +335,7 @@
                 echo " <INPUT TYPE=hidden NAME=wdir VALUE=\"$wdir\">";
                 echo " <INPUT TYPE=hidden NAME=file VALUE=\"$file\">";
                 echo " <INPUT TYPE=hidden NAME=action VALUE=edit>";
-                print_textarea($usehtmleditor, 25, 80, 680, 400, "text", $contents);
+                print_textarea($usehtmleditor, 25, 80, 680, 400, "text", addslashes($contents));
                 echo "</TD></TR><TR><TD>";
                 echo " <INPUT TYPE=submit VALUE=\"".get_string("savechanges")."\">";
                 echo "</FORM>";