diff options
Diffstat (limited to 'CIAO/bin/replace_dummy_with_dummylabel.sh')
| -rwxr-xr-x | CIAO/bin/replace_dummy_with_dummylabel.sh | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/CIAO/bin/replace_dummy_with_dummylabel.sh b/CIAO/bin/replace_dummy_with_dummylabel.sh deleted file mode 100755 index 3f699576154..00000000000 --- a/CIAO/bin/replace_dummy_with_dummylabel.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/bin/bash -find . -name "*.mpc" > mpc_files -for i in `cat mpc_files` -do - sed -e 's/requires += dummy$/requires += dummy_label/g' $i > tmp - cat tmp > $i -done - -rm -f mpc_files -rm -f tmp |