diff options
Diffstat (limited to 'gdb/config/.Sanitize')
| -rw-r--r-- | gdb/config/.Sanitize | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/gdb/config/.Sanitize b/gdb/config/.Sanitize index e51c3d5..4025e8b 100644 --- a/gdb/config/.Sanitize +++ b/gdb/config/.Sanitize @@ -63,6 +63,20 @@ else fi fi +tic80_files="tic80" + +if ( echo $* | grep keep\-tic80 > /dev/null ) ; then + keep_these_too="${tic80_files} ${keep_these_too}" + if [ -n "${verbose}" ] ; then + echo Keeping ${tic80_files} + fi +else + lose_these_too="${tic80_files} ${lose_these_too}" + if [ -n "${verbose}" ] ; then + echo Deleting ${tic80_files} + fi +fi + # All files listed between the "Things-to-keep:" line and the # "Files-to-sed:" line will be kept. All other files will be removed. # Directories listed in this section will have their own Sanitize |