/bin/sed works on both Solaris and RedHat Linux; /usr/bin/sed does not.

diff --git a/Doc/tools/fix_libaux.sed b/Doc/tools/fix_libaux.sed
index 459b7e8d3658478d4bafec157c252212edf8d17b..fb33cc575de249c5cf8892ad3c6d02ca071f2914 100755 (executable)
--- a/Doc/tools/fix_libaux.sed
+++ b/Doc/tools/fix_libaux.sed
@@ -1,3 +1,3 @@
-#! /usr/bin/sed -f
+#! /bin/sed -f
 s/{\\tt  \\hackscore  {}\\hackscore  {}/\\sectcode{__/
 s/\\hackscore  {}\\hackscore  {}/__/