From 72eeead8935ddf733022b2427c2cf2797126f570 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 30 Apr 2012 13:17:14 +0000
Subject: Change default Unicode Tokens font back to DejaVU Sans, more reliable
 without installing STIX.

---
 isar/Example-Tokens.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'isar')

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
index 2106ccaf..46c9a2cc 100644
--- a/isar/Example-Tokens.thy
+++ b/isar/Example-Tokens.thy
@@ -4,7 +4,7 @@
       View and process this document with Unicode Tokens engaged.
    
       For a more exhaustive test of token display, visit the test
-      file etc/isar/TokensAcid.thy
+      file etc/isar/TokensAcid.thy.  Check the FAQ for more advice.
 
       $Id$
 *)
-- 
cgit v1.2.3