title: Add leading zeroes to awk variable
body: <p>I have the following awk command within a "for" loop in bash:</p>
  
  <pre><code>awk -v pdb="$pdb" 'BEGIN {file = 1; filename = pdb"_" file ".pdb"}
   /ENDMDL/ {getline; file ++; filename = pdb"_" file ".pdb"}
   {print $0 &gt; filename}' &lt; ${pdb}.pdb 
  </code></pre>
  
  <p>This reads a series of files with the name $pdb.pdb and splits them in files called $pdb_1.pdb, $pdb_2.pdb, ..., $pdb_21.pdb, etc. However, I would like to produce files with names like $pdb_01.pdb, $pdb_02.pdb, ..., $pdb_21.pdb, i.e., to add padding zeros to the "file" variable. </p>
  
  <p>I have tried without success using printf in different ways. Help would be much appreciated.</p>