From ace8d56c1782710841404915cf376db1586d765f Mon Sep 17 00:00:00 2001
From: Arnaud Legrand <arnaud.legrand@imag.fr>
Date: Tue, 26 Mar 2019 12:41:36 +0100
Subject: [PATCH] [HTML] Stupid me. I had forgotten to reactivate pandoc
 generation

---
 bin/pandoc_fixer.pl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/pandoc_fixer.pl b/bin/pandoc_fixer.pl
index 810de0f..bc5f8f3 100755
--- a/bin/pandoc_fixer.pl
+++ b/bin/pandoc_fixer.pl
@@ -112,7 +112,7 @@ sub main() {
 	my($file,$url) = split(/\s*#\s*/,$f);
 	if($file eq "" || !defined($url)) { warn "Malformed line"; next;}
 	# print "'$file' --- '$url'\n";
-#	pandoc_export($file);
+	pandoc_export($file);
 
 	my($html)=$file;     $html=~ s/\.[^\.]*$/.html/g;
 	my($url_id) = $url;  $url_id =~ s|^.*jump_to_id/||g;
-- 
2.18.1