2018-10-21 22:32:24 +01:00
|
|
|
#!/bin/bash
|
2018-10-19 19:35:56 +01:00
|
|
|
|
2018-10-21 22:32:24 +01:00
|
|
|
TMP1="trampolines-raw.out"
|
|
|
|
TMP2="trampolines.out"
|
|
|
|
|
|
|
|
make clean ; make 2>$TMP1
|
|
|
|
cat $TMP1 | grep "warning: trampoline" | sort -u > $TMP2
|
|
|
|
cat $TMP2
|
2018-10-19 19:35:56 +01:00
|
|
|
echo
|
2018-10-21 22:32:24 +01:00
|
|
|
wc -l $TMP2
|
2018-10-19 19:35:56 +01:00
|
|
|
|