etc/settings
changeset 14981 e73f8140af78
parent 14943 ffdb22cf6f67
child 15218 39747a9e3c37
equal deleted inserted replaced
14980:267cc670317a 14981:e73f8140af78
     1 # -*- shell-script -*-
     1 # -*- shell-script -*-
     2 # $Id$
     2 # $Id$
     3 # Author: Markus Wenzel, TU Muenchen
     3 # Author: Markus Wenzel, TU Muenchen
     4 # License: GPL (GNU GENERAL PUBLIC LICENSE)
       
     5 #
     4 #
     6 # Isabelle settings -- site defaults.
     5 # Isabelle settings -- site defaults.
     7 # Do *NOT* copy this file into your personal isabelle directory!!!
     6 # Do *NOT* copy this file into your personal isabelle directory!!!
     8 
     7 
     9 ###
     8 ###