Committed to enable merge.

[splint.git] / src / Headers / rcfiles.h

diff --git a/src/Headers/rcfiles.h b/src/Headers/rcfiles.h
new file mode 100644 (file)
index 0000000..fa0e0aa
--- /dev/null
+++ b/src/Headers/rcfiles.h
@@ -0,0 +1,18 @@
+/*
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** See ../LICENSE for license information.
+**
+*/
+/*
+** rcfiles.h
+*/
+
+# ifndef RCFILES_H
+# define RCFILES_H
+
+extern bool rcfiles_read (cstring p_fname,
+                         cstringSList *p_passThroughArgs,
+                         bool p_report) 
+  /*@modifies fileSystem, internalState, *p_passThroughArgs@*/ ;
+   
+# endif