Admin/fixencoding
changeset 2966 09e87e779b7d
parent 2946 3178e9a44d3c
child 4499 4ca67338e22c
equal deleted inserted replaced
2965:afbda7e26f15 2966:09e87e779b7d
     1 #!/usr/bin/perl -w
     1 #!/usr/local/dist/bin/perl -w
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # fixencoding - fix references to isabelle font encoding
     5 # fixencoding - fix references to isabelle font encoding
     6 
     6