| author | wenzelm | 
| Fri, 18 Jul 1997 13:37:16 +0200 | |
| changeset 3530 | d9ca80f0759c | 
| parent 903 | 26138063bb88 | 
| permissions | -rwxr-xr-x | 
| 903 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 1 | #! /bin/csh | 
| 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 2 | # $Id$ | 
| 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 3 | # Find all "orphan" ML-files (those with no thy-file) | 
| 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 4 | foreach f (*.ML) | 
| 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 5 | if ( ! -f $f:r.thy ) echo $f | 
| 
26138063bb88
New shell script for finding orphan .ML files (those with no
 lcp parents: diff
changeset | 6 | end |