diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 21:50:13 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 21:50:13 +0000 |
| commit | 9ec64a6cfd422fa0ad76c7971fa47d0beb15bf19 (patch) | |
| tree | 69ca59fd2e240133630aa88d231fd4b13eb5e650 /contrib | |
| parent | 4e62744f9c95906c69696ed0a0d46269ecb83381 (diff) | |
Adding documentation to my-configure
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/my-configure | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/my-configure b/contrib/my-configure index dce46fc67..65a64895d 100755 --- a/contrib/my-configure +++ b/contrib/my-configure @@ -1,3 +1,6 @@ +# Includes the contents of the file .cvc4_config, if it exists, +# on the ./configure command line + #! /bin/bash CONFIG_OPTIONS= |