From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 7 Feb 2004 19:31:13 +0000
Subject: Deleted file

---
 html/userman | 3 ---
 1 file changed, 3 deletions(-)
 delete mode 100644 html/userman

(limited to 'html/userman')

diff --git a/html/userman b/html/userman
deleted file mode 100644
index e8ccc072..00000000
--- a/html/userman
+++ /dev/null
@@ -1,3 +0,0 @@
-<?php require('functions.php3');
-      hack_html("ProofGeneral/doc/ProofGeneral_toc.html","Proof General user manual","userman");
-?>
-- 
cgit v1.2.3