aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2012-04-30 13:17:14 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2012-04-30 13:17:14 +0000
commit72eeead8935ddf733022b2427c2cf2797126f570 (patch)
tree1b47a3e3c118b6fb1367f9d516db1ea64435a7bd /isar
parentef584b51fac4be9703d8772b3c20bbeffc5f9fc8 (diff)
Change default Unicode Tokens font back to DejaVU Sans, more reliable without installing STIX.
Diffstat (limited to 'isar')
-rw-r--r--isar/Example-Tokens.thy2
1 files changed, 1 insertions, 1 deletions
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$
*)