Merge pull request #1933 from dedis/work-bug-daniel-embedme

fix embedme not working

docs/embedme.sh

@@ -34,7 +34,7 @@ BEGIN {
 {
     # if this is a closing block line, unsets the del variable to stop deleting
     # lines if it was the case
-    if ($0 ~ /^\`\`\`$/) {
+    if ($0 ~ /^```$/) {
         del=0;
         print $0;
 
@@ -44,15 +44,14 @@ BEGIN {
 
     # if this is the start of an opening block, we indicate that with the
     # last_line variable
-    } else if ($0 ~ /\`\`\`json5/) {
+    } else if ($0 ~ /```json5/) {
         last_line=1;
         print $0;
 
     # if the previous line was an opening block, and we get a comment, then
     # let's fill the block with the file's content and remove the old lines from
     # the block. $1 will contain "//" and $2 will contain the filename.
     } else if ($0 ~ /\/\/ .+\.json/ && last_line == 1) {
-
         # check if the file exists.
         if (system("test -f " $2)==0) {
             print $0;