diff options
| author | Hugo Herbelin | 2016-07-31 07:51:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-08-17 10:32:47 +0200 |
| commit | 6afe9005b2f050e04f897ed7e84014058fc94e4b (patch) | |
| tree | 9cbc764307dbccf550246ca25ecc7b9bb8c362f8 /dev | |
| parent | 303f644773969ff84d167e3361c6bb9f9545e8bf (diff) | |
A fix to dev/include.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/include b/dev/include index b2eb280d6c..d82fb74f22 100644 --- a/dev/include +++ b/dev/include @@ -25,7 +25,7 @@ #cd ".";; #use "base_include";; -#install_printer (* pp_stdcmds *) pppp;; +#install_printer (* pp_stdcmds *) pp;; #install_printer (* pattern *) pppattern;; #install_printer (* glob_constr *) ppglob_constr;; |