Add integral extension glyph.

Add new option `-x' to afmtodit to suppress use of built-in AGL.

* font/devhtml/R.proto, font/devutf8/R.proto: Add `u23AE'.

* font/devps/generate/textmap: Provide entry for `integralex' to
override (old) PUA value of the AGL.
* font/devps/generate/Makefile (SS): Add afmtodit option `-x'.
* font/devps/*: Regenerated.

* src/utils/afmtodit/afmtodit.pl: Add option `-x'.
* src/utils/afmtodit/afmtodit.man, NEWS: Updated.

1 files changed, 13 insertions, 0 deletions

diff --git a/font/devps/HR b/font/devps/HR
index 469f47f8..cbf1ab80 100644
--- a/font/devps/HR
+++ b/font/devps/HR
@@ -143,6 +143,7 @@ b , -40
 b b -10
 c k -20
 c , -15
+: u0020 -50
 , ' -100
 , cq -100
 , rq -100
@@ -207,13 +208,17 @@ o , -40
 p y -30
 p . -35
 p , -35
+. u0020 -60
 . ' -100
 . cq -100
 . rq -100
+rq u0020 -40
 ` ` -57
 ` oq -57
 oq ` -57
 oq oq -57
+' u0020 -70
+cq u0020 -70
 ' s -50
 cq s -50
 ' r -50
@@ -242,6 +247,14 @@ r a -10
 s w -30
 s . -15
 s , -15
+; u0020 -50
+u0020 ` -60
+u0020 oq -60
+u0020 lq -30
+u0020 Y -90
+u0020 W -40
+u0020 V -50
+u0020 T -50
 v . -80
 v o -25
 v e -25