From 9cdf9c3c0341a395249946d9e8f0bed7dd3c6d53 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Dec 2008 14:38:55 +0000
Subject: - coq_makefile: target install now respects the original tree
 structure   of the archive to install in coq user-contrib installation
 directory. - Relaxed the validity check on identifiers from an error to a
 warning. - Added a filtering option to Print LoadPath. - Support for empty
 root in option -R. - Better handling of redundant paths in ml loadpath. -
 Makefile's: Added target initplugins and added initplugins to coqbinaries.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6d6a0c0656..02f36a8c88 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1886,7 +1886,8 @@ let rec xlate_vernac =
 	| PrintHint id ->
 	    CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
 	| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
-	| PrintLoadPath -> CT_print_loadpath
+	| PrintLoadPath None -> CT_print_loadpath
+	| PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir"
 	| PrintMLLoadPath -> CT_ml_print_path
 	| PrintMLModules -> CT_ml_print_modules
 	| PrintGraph -> CT_print_graph
-- 
cgit v1.2.3