2015-04-13 19:32:00

1 files changed, 14 insertions, 7 deletions

diff --git a/tex/context/base/font-ctx.lua b/tex/context/base/font-ctx.lua
index a58a3b9d6..2c96e9ac2 100644
--- a/tex/context/base/font-ctx.lua
+++ b/tex/context/base/font-ctx.lua
@@ -1292,13 +1292,9 @@ do  -- else too many locals
         end
     end
 
-end
-
--- local id, cs = fonts.definers.internal { }
--- local id, cs = fonts.definers.internal { number = 2 }
--- local id, cs = fonts.definers.internal { name = "dejavusans" }
-
-do
+    -- local id, cs = fonts.definers.internal { }
+    -- local id, cs = fonts.definers.internal { number = 2 }
+    -- local id, cs = fonts.definers.internal { name = "dejavusans" }
 
     local n = 0
 
@@ -1334,6 +1330,17 @@ do
         return id, csnames[id]
     end
 
+    -- here
+
+    local infofont = 0
+
+    function fonts.infofont()
+        if infofont == 0 then
+            infofont = definers.define { name = "dejavusansmono", size = tex.sp("6pt") }
+        end
+        return infofont
+    end
+
 end
 
 local enable_auto_r_scale = false