diff --git a/2001/herrmann2/.gitignore b/2001/herrmann2/.gitignore index 188889829..981ac5f50 100644 --- a/2001/herrmann2/.gitignore +++ b/2001/herrmann2/.gitignore @@ -4,6 +4,7 @@ cup.out cup.out2 herrmann2 +herrmann2.alt herrmann2.orig indent indent.c diff --git a/bin/sgi.sh b/bin/sgi.sh index 29e6ffb07..016a38d17 100755 --- a/bin/sgi.sh +++ b/bin/sgi.sh @@ -47,5 +47,5 @@ # Share and enjoy! :-) sed -e '/^#/s/.*/0 &/' -e '/^*/s/.*/1 &/' -e '/^[^01*!]/s/.*/2 &/' -e '/^!/s/.*/3 &/' | - sort -k 1n -k 2d | + sort -u -k 1n -k 2d | sed 's/[0123] //'