diff src/settings.sig @ 1096:324c9ffe8ff9

Protocol-specific compiler options
author Adam Chlipala <adamc@hcoop.net>
date Sun, 27 Dec 2009 14:25:22 -0500
parents bed675db3aff
children 01b6c7144a44
line wrap: on
line diff
--- a/src/settings.sig	Sun Dec 27 13:18:32 2009 -0500
+++ b/src/settings.sig	Sun Dec 27 14:25:22 2009 -0500
@@ -93,6 +93,7 @@
     (* Web protocols that generated programs may speak *)
     type protocol = {
         name : string,       (* Call it this on the command line *)
+        compile : string,    (* Pass these `gcc -c' arguments *)
         linkStatic : string, (* Pass these static linker arguments *)
         linkDynamic : string,(* Pass these dynamic linker arguments *)
         persistent : bool    (* Multiple requests per process? *)