diff --git a/mod/resource/type/file/resource.class.php b/mod/resource/type/file/resource.class.php index f5429d79df5..175d7e9dcfd 100644 --- a/mod/resource/type/file/resource.class.php +++ b/mod/resource/type/file/resource.class.php @@ -223,6 +223,10 @@ function display() { } else if ($mimetype == "audio/mp3") { // It's an MP3 audio file $resourcetype = "mp3"; $embedded = true; + + } else if ($mimetype == "video/x-flv") { // It's a Flash video file + $resourcetype = "flv"; + $embedded = true; } else if (substr($mimetype, 0, 10) == "video/x-ms") { // It's a Media Player file $resourcetype = "mediaplayer"; @@ -453,6 +457,38 @@ function display() { echo ''; echo ''; echo ''; + echo '
'; + + echo ''; + echo ''; + + } else if ($resourcetype == "flv") { + $id = 'filter_flv_'.time(); //we need something unique because it might be stored in text cache + $cleanurl = addslashes_js($fullurl); + + + // If we have Javascript, use UFO to embed the FLV player, otherwise depend on plugins + + echo '