src/Tools/jEdit/dist-template/interface
changeset 34411 0e49a2edadea
parent 34409 e61e2ab1f6f7
child 34412 c60770179a0c
equal deleted inserted replaced
34410:f2644d2a3e8e 34411:0e49a2edadea
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 #
     2 #
     3 # Isabelle/jEdit interface wrapper
     3 # Isabelle/jEdit interface wrapper
     4 
       
     5 set -x
       
     6 
     4 
     7 ## diagnostics
     5 ## diagnostics
     8 
     6 
     9 usage()
     7 usage()
    10 {
     8 {