diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py index 146175562e7b5415b9c275414b53324594789ff8..dd7c7af6e4941f7aaac1366860fe92ae45388d47 100755 --- a/share/analysis-scripts/summary.py +++ b/share/analysis-scripts/summary.py @@ -122,10 +122,10 @@ def terminate_process(process): def smart_rename(target): - target = re.sub("^\./", "", target) - target = re.sub("main\.eva$", "", target) - target = re.sub("\.eva$", "", target) - target = re.sub("\.frama-c/", "", target) + target = re.sub(r"^\./", "", target) + target = re.sub(r"main\.eva$", "", target) + target = re.sub(r"\.eva$", "", target) + target = re.sub(r"\.frama-c/", "", target) return target