etc/user-settings.sample
changeset 3749 8a8ed98bd2ca
parent 3289 8c947c178f29
child 7856 7d06972db6ca
equal deleted inserted replaced
3748:e5d2399a154f 3749:8a8ed98bd2ca
     7 
     7 
     8 ###
     8 ###
     9 ### Compilation options
     9 ### Compilation options
    10 ###
    10 ###
    11 
    11 
    12 #ISABELLE_USEDIR_OPTIONS="-h true -g true"
    12 #ISABELLE_USEDIR_OPTIONS="-i true"
    13 
    13 
    14 
    14 
    15 ###
    15 ###
    16 ### Heap files
    16 ### Heap files
    17 ###
    17 ###