From d46e373d64b43c95e5292f958e2a864fe370055d Mon Sep 17 00:00:00 2001
From: benweet <benoit.schweblin@gmail.com>
Date: Thu, 12 Jun 2014 21:14:20 +0100
Subject: [PATCH] Changed default highlighter to highlight.js

---
 public/res/extensions/markdownExtra.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/public/res/extensions/markdownExtra.js b/public/res/extensions/markdownExtra.js
index d42d17d4..b91c60b8 100644
--- a/public/res/extensions/markdownExtra.js
+++ b/public/res/extensions/markdownExtra.js
@@ -27,7 +27,7 @@ define([
 		],
 		intraword: true,
 		comments: true,
-		highlighter: "prettify"
+		highlighter: "highlight"
 	};
 
 	markdownExtra.onLoadSettings = function() {