Fixes Fatal error: Call to undefined function repository_head_setup()

diff --git a/lib/form/editor.php b/lib/form/editor.php
index 1da0ec0b4699ec0a655b49f0cc81ac115f8a1679..aa412d0c11d11bfb603c57db976effd48dfb156c 100644 (file)
--- a/lib/form/editor.php
+++ b/lib/form/editor.php
@@ -4,6 +4,7 @@ global $CFG;
 
 require_once('HTML/QuickForm/element.php');
 require_once($CFG->dirroot.'/lib/filelib.php');
+require_once($CFG->dirroot.'/repository/lib.php');
 
 //TODO:
 //  * locking