diff options
Diffstat (limited to 'docs/Makefile.in')
| -rw-r--r-- | docs/Makefile.in | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/docs/Makefile.in b/docs/Makefile.in index 01fc1e56..295d3a02 100644 --- a/docs/Makefile.in +++ b/docs/Makefile.in @@ -1196,6 +1196,7 @@ mkdir_p = @mkdir_p@ neqn = @neqn@ nroff = @nroff@ oldincludedir = @oldincludedir@ +override_dir = @override_dir@ pager = @pager@ pdfdir = @pdfdir@ pic = @pic@ |