diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/Makefile.template | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/config/Makefile.template b/config/Makefile.template index 16dc75894..67c4c34d1 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -133,6 +133,11 @@ HASCOQIDE=COQIDEOPT # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE +# Defining options to generate dependencies graphs +DOT=dot +DOTOPTS=-Tps +ODOCDOTOPTS=-dot -dot-reduce + # make or sed are bogus and believe lines not terminating by a return # are inexistent |