equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
|
3 # $Id$ |
|
4 # |
3 # Emacs / Isamode interface. |
5 # Emacs / Isamode interface. |
4 # |
|
5 # $Id$ |
|
6 # |
6 # |
7 # TODO: isabelle fonts |
7 # TODO: isabelle fonts |
8 |
8 |
9 |
9 |
10 ## diagnostics |
10 ## diagnostics |