# HG changeset patch
# User wenzelm
# Date 1126642791 -7200
# Node ID 325707c676e225a769ae63f686addebd32d754b3
# Parent  a8e19032497db4a8aace6a0a537445f5b2c9506c
export ml_exts;

diff -r a8e19032497d -r 325707c676e2 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Sep 13 22:19:50 2005 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Sep 13 22:19:51 2005 +0200
@@ -20,6 +20,7 @@
 sig
   include BASIC_THY_LOAD
   val cond_add_path: Path.T -> ('a -> 'b) -> 'a -> 'b
+  val ml_exts: string list
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
   val check_file: Path.T option -> Path.T -> (Path.T * File.info) option