diff -r 1134ee401b20 -r cc57255bf6ae etc/settings
--- a/etc/settings	Sat Aug 13 23:33:58 2016 +0200
+++ b/etc/settings	Sat Aug 13 23:45:29 2016 +0200
@@ -132,6 +132,8 @@
 ### Misc settings
 ###
 
+ISABELLE_GNUPLOT="gnuplot"
+
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_OCAML="/usr/bin/ocaml"
 #ISABELLE_SWIPL="/usr/bin/swipl"