diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/Makefile.template | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index a3465722f..d4fa11783 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -15,6 +15,9 @@ # ############################################################################# +#Variable used to detect whether ./configure has run successfully. +COQ_CONFIGURED=yes + # Local use (no installation) LOCAL=LOCALINSTALLATION |