diff src/config.sig @ 1523:52fbd8534ef3

Remove some GCC-specific identifier choice and documentation
author Adam Chlipala <adam@chlipala.net>
date Tue, 02 Aug 2011 14:45:19 -0400
parents b5517f47b1f1
children 7770ef82c463
line wrap: on
line diff
--- a/src/config.sig	Tue Aug 02 14:31:37 2011 -0400
+++ b/src/config.sig	Tue Aug 02 14:45:19 2011 -0400
@@ -9,7 +9,7 @@
     val libJs : string
 
     val ccompiler : string
-    val gccArgs : string
+    val ccArgs : string
     val openssl : string
 
     val pgheader : string