aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-07 08:52:24 +0000
committerDavid Aspinall2009-09-07 08:52:24 +0000
commitaa757ce580f4c97e6f18a3f28759897b587586c9 (patch)
tree552e7fe0b357470611677738f7218901d1528706
parent70d3abea45c00e0ee6394941e020bb63bc070d8e (diff)
Missing require
-rw-r--r--generic/pg-user.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 34afcf0e..2dc04816 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1,6 +1,6 @@
;;; pg-user.el --- User level commands for Proof General
;;
-;; Copyright (C) 2000-2008 LFCS Edinburgh.
+;; Copyright (C) 2000-2009 LFCS Edinburgh.
;; Author: David Aspinall and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
@@ -16,6 +16,8 @@
;;; Code:
(require 'span)
+(require 'scomint)
+
(require 'proof) ; loader
(require 'proof-script) ; we build on proof-script