Added option to choose HTML editor

diff --git a/user/edit.html b/user/edit.html
index ed9669174bda7e22aef7688e30268ac8f5c29b63..11a694497042a9f472d392373fc4d1865df20e5c 100644 (file)
--- a/user/edit.html
+++ b/user/edit.html
@@ -61,6 +61,15 @@ if (isadmin()) {
     choose_from_menu ($choices, "mailformat", $user->mailformat, "") ?>
        </td>
 </tr>
+<tr valign=top>
+       <td><P><? print_string("textediting") ?>:</td>
+       <td><? 
+    unset($choices);
+    $choices["0"] = get_string("texteditor");
+    $choices["1"] = get_string("htmleditor");
+    choose_from_menu ($choices, "htmleditor", $user->htmleditor, "") ?>
+       </td>
+</tr>
 <tr valign=top>
        <td><P><? print_string("city") ?>:</td>
        <td><input type="text" name="city" size=25 value="<? p($user->city) ?>">