equal
deleted
inserted
replaced
1 #!/bin/bash -x |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution. |
5 # makerpm -- make Isabelle rpm packages for Linux/x86 from the distribution. |
6 |
6 |