From 9534a90440aa813824eba17ed17d9d62832d35dc Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 24 Apr 2004 11:07:12 +0000
Subject: Spacing

---
 doc/PG-adapting.texi | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index f4fbe1cc..86cc1601 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1933,8 +1933,6 @@ scripting (to do undo operations), the whole history is discarded.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-shell-require-command-regexp
-
-
 @defvar proof-shell-require-command-regexp 
 A regular expression to match a Require-type of command, or nil.@*
 If set to a regexp, then @samp{@code{proof-done-advancing-require-function}}
@@ -1944,11 +1942,8 @@ This can be used to adjust @samp{@code{proof-included-files-list}} based on the
 lines of script that have been processed/parsed, rather than relying
 on information from the prover.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function
-
-
-
 
+@c TEXI DOCSTRING MAGIC: proof-done-advancing-require-function
 @defvar proof-done-advancing-require-function 
 Invoked from @samp{@code{proof-done-advancing}}, see @samp{@code{proof-shell-require-command-regexp}}.@*
 The function is passed the span and the command as arguments.
-- 
cgit v1.2.3