Update FAQ_DEV.

diff --git a/doc/FAQ_DEV b/doc/FAQ_DEV
index 0de0d6407c9b5e387319bad81045faf6182e76ba..9481c36b38938a1d976ed8f948c83c24b610167d 100644 (file)
--- a/doc/FAQ_DEV
+++ b/doc/FAQ_DEV
@@ -80,7 +80,8 @@
    glimpse.
    
    make_diff has tools to create patch diff files that can be applied to
-   the distribution.
+   the distribution. This produces context diffs, which is our preferred
+   format.
    
    Our standard format is to indent each code level with one tab, where
    each tab is four spaces. You will need to set your editor to display

diff --git a/doc/src/FAQ/FAQ_DEV.html b/doc/src/FAQ/FAQ_DEV.html
index 3b302172184f52716aa5066d5f5c9360f3e8ccdb..179f6168438eba62dd68bd71e77323614d7169ed 100644 (file)
--- a/doc/src/FAQ/FAQ_DEV.html
+++ b/doc/src/FAQ/FAQ_DEV.html
@@ -112,7 +112,8 @@
     Others prefer <I>glimpse.</I> 
 
     <P><I>make_diff</I> has tools to create patch diff files that can
-    be applied to the distribution.</P>
+    be applied to the distribution.  This produces context diffs, which
+    is our preferred format.</P>
 
     <P>Our standard format is to indent each code level with one tab,
     where each tab is four spaces. You will need to set your editor to