diff options
Diffstat (limited to 'Master/tlpkg/bin/ctan2tl')
-rwxr-xr-x | Master/tlpkg/bin/ctan2tl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Master/tlpkg/bin/ctan2tl b/Master/tlpkg/bin/ctan2tl index d0765d8ce49..e1360d71564 100755 --- a/Master/tlpkg/bin/ctan2tl +++ b/Master/tlpkg/bin/ctan2tl @@ -59,6 +59,12 @@ fi echo "$0: ctan dir for $pkg" echo "$0: is $ctan_dir1" +if grep " $pkg " $mydir/tlpkg-ctan-check >/dev/null; then :; else + echo + echo "$0: $pkg not in $mydir/tlpkg-ctan-check, add?" +fi + +# if $copy_from_ctan; then # remove whatever dregs in raw that might be lying around. |