diff options
Diffstat (limited to 'src/lib/make.bash')
| -rwxr-xr-x | src/lib/make.bash | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/lib/make.bash b/src/lib/make.bash index 5714954fa8..6277c93f83 100755 --- a/src/lib/make.bash +++ b/src/lib/make.bash @@ -6,8 +6,6 @@ set -e -echo; echo; echo %%%% making lib %%%%; echo - for i in os math do echo; echo; echo %%%% making lib/$i %%%%; echo |