diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-17 19:12:43 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-17 19:12:43 +0000 |
commit | 1dfb57de029dbef0b5d05561891f841b5ba87291 (patch) | |
tree | af5e68857b43c84a175dc3f5c692bc38213821cb /Makefile.reconf_args | |
parent | d4e7b9cce6947498738bd3cfb67c11e3bf6c8dbe (diff) |
coding standard fix on SmtEngine; fix recursive make
Diffstat (limited to 'Makefile.reconf_args')
-rw-r--r-- | Makefile.reconf_args | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.reconf_args b/Makefile.reconf_args index 10d3c84b9..516ae0adb 100644 --- a/Makefile.reconf_args +++ b/Makefile.reconf_args @@ -1,3 +1,4 @@ +# -*-makefile-*- # This makefile snippet maps make-time arguments to configure and # build-type arguments # |