diff --git a/.gitignore b/.gitignore index 20e0c051d6..194bb11f0d 100644 --- a/.gitignore +++ b/.gitignore @@ -32,6 +32,7 @@ timing.log *_thm.txt *_ast.txt *.ml.txt +*translate_timing.txt # Emacs backup files *~