Run lint script handling deleted files#428

peterschrammel merged 1 commit intodiffblue:masterdiffblue/cbmc:masterfrom

thk123:bug/deleted-file-lintthk123/cbmc:bug/deleted-file-lintCopy head branch name to clipboard