diff options
Diffstat (limited to 'config/var-def.mk')
| -rw-r--r-- | config/var-def.mk | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/config/var-def.mk b/config/var-def.mk index 542b0bc2..a4dc07e8 100644 --- a/config/var-def.mk +++ b/config/var-def.mk @@ -149,6 +149,7 @@ axiom_src_srcdir = $(top_srcdir)/src axiom_src_docdir = $(axiom_src_srcdir)/doc axiom_src_datadir = $(axiom_src_srcdir)/share axiom_src_algdir = $(axiom_src_srcdir)/algebra +axiom_src_texdir = $(axiom_src_datadir)/tex ## Where tools for the build machine are built # Tools that we occasionally build don't know |