diff options
Diffstat (limited to 'Build')
-rwxr-xr-x | Build/cdbuild/ctan2tds.pl | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Build/cdbuild/ctan2tds.pl b/Build/cdbuild/ctan2tds.pl index 1e5dcc2ba9b..eff5b5d30f7 100755 --- a/Build/cdbuild/ctan2tds.pl +++ b/Build/cdbuild/ctan2tds.pl @@ -293,8 +293,9 @@ chdir $startdir || die "chdir($startdir) failed: $!"; 'showexpl', "&MAKEflatten", 'siam', "&MAKEsiam", 'skak', "&MAKEflatten", + 'songs', "print \"skipping symbolindex, requires binary\"", 'stellenbosch',"&MAKEcopy", - 'symbolindex', "print \"skipping symbolindex, requires binary, skip\"", + 'symbolindex', "print \"skipping symbolindex, requires binary\"", 't2', "&MAKEt2", 'tabvar', "&MAKEflatten", 'tamethebeast',"&MAKEtamethebeast", |