etc/settings
changeset 73224 49686e3b1909
parent 73180 14f8db6746cb
child 73261 f0446b3e4d17
--- a/etc/settings	Mon Feb 01 18:12:44 2021 +0100
+++ b/etc/settings	Wed Feb 03 20:18:34 2021 +0100
@@ -112,7 +112,7 @@
 
 
 ###
-### Docs
+### Docs and external files
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
@@ -136,6 +136,8 @@
 
 PDF_VIEWER="$ISABELLE_OPEN"
 
+ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp"
+
 
 ###
 ### Symbol rendering